*##################################
*this is the only problem remaining :)
d114::eqid         |- ( x e. CC |-> ( x / ( B - A ) ) ) = ( x e. CC |-> ( x / ( B - A ) ) )
212f:d114:divccncf |- ( ( ( B - A ) e. CC /\ ( B - A ) =/= 0 ) -> ( x e. CC |-> ( x / ( B - A ) ) ) e. ( CC -cn-> CC ) )
212k::rescncf      |- ( ( A [,] B ) C_ CC -> ( ( x e. CC |-> ( x / ( B - A ) ) ) e. ( CC -cn-> CC ) -> ( ( x e. CC |-> ( x / ( B - A ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
212l::resmpt       |- ( ( A [,] B ) C_ CC -> ( ( x e. CC |-> ( x / ( B - A ) ) ) |` ( A [,] B ) ) = ( x e. ( A [,] B ) |-> ( x / ( B - A ) ) ) )
212m:16a,24,212f:mp2an |- ( x e. CC |-> ( x / ( B - A ) ) ) e. ( CC -cn-> CC )
212n:15b,212m,212k:mp2 |- ( ( x e. CC |-> ( x / ( B - A ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC )
212o:15b,212l:ax-mp |- ( ( x e. CC |-> ( x / ( B - A ) ) ) |` ( A [,] B ) ) = ( x e. ( A [,] B ) |-> ( x / ( B - A ) ) )
212p:212o,212n:eqeltrri |- ( x e. ( A [,] B ) |-> ( x / ( B - A ) ) ) e. ( ( A [,] B ) -cn-> CC )
d115:15b:sseli     |- ( x e. ( A [,] B ) -> x e. CC )
d116:10ac:a1i      |- ( x e. ( A [,] B ) -> A e. CC )
d117:16a:a1i       |- ( x e. ( A [,] B ) -> ( B - A ) e. CC )
d118:24:a1i        |- ( x e. ( A [,] B ) -> ( B - A ) =/= 0 )
212g:d115,d116,d117,d118:divsubdird |- ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) = ( ( x / ( B - A ) ) - ( A / ( B - A ) ) ) )
d120:212g:adantl   |- ( ( T. /\ x e. ( A [,] B ) ) -> ( ( x - A ) / ( B - A ) ) = ( ( x / ( B - A ) ) - ( A / ( B - A ) ) ) )
212h:d120:mpteq2dva |- ( T. -> ( x e. ( A [,] B ) |-> ( ( x - A ) / ( B - A ) ) ) = ( x e. ( A [,] B ) |-> ( ( x / ( B - A ) ) - ( A / ( B - A ) ) ) ) )
d123:212p:a1i      |- ( T. -> ( x e. ( A [,] B ) |-> ( x / ( B - A ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
212j::cncfmptc     |- ( ( ( A / ( B - A ) ) e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC ) -> ( x e. ( A [,] B ) |-> ( A / ( B - A ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
d126:10ac,16a,24:divcli |- ( A / ( B - A ) ) e. CC
d125:d126,15b,211,212j:mp3an |- ( x e. ( A [,] B ) |-> ( A / ( B - A ) ) ) e. ( ( A [,] B ) -cn-> CC )
d124:d125:a1i         |- ( T. -> ( x e. ( A [,] B ) |-> ( A / ( B - A ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
212i:d77,d78,d123,d124:cncfmpt2f |- ( T. -> ( x e. ( A [,] B ) |-> ( ( x / ( B - A ) ) - ( A / ( B - A ) ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
212e:212h,212i:eqeltrd |- ( T. -> ( x e. ( A [,] B ) |-> ( ( x - A ) / ( B - A ) ) ) e. ( ( A [,] B ) -cn-> CC ) )