let A, B, C, D be real number ; :: thesis: for f being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for t being Point of (TOP-REAL 2) holds f . t = |[((A * (t `1 )) + B),((C * (t `2 )) + D)]| ) holds
f is continuous
let f be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis: ( ( for t being Point of (TOP-REAL 2) holds f . t = |[((A * (t `1 )) + B),((C * (t `2 )) + D)]| ) implies f is continuous )
assume A1: for t being Point of (TOP-REAL 2) holds f . t = |[((A * (t `1 )) + B),((C * (t `2 )) + D)]| ; :: thesis: f is continuous
A2: (TOP-REAL 2) | ([#] (TOP-REAL 2)) = TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) by TSEP_1:100;
then reconsider f1 = proj1 * f as Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 by TOPMETR:24;
reconsider f2 = proj2 * f as Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 by A2, TOPMETR:24;
reconsider f0 = f as Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),((TOP-REAL 2) | ([#] (TOP-REAL 2))) by A2;
set K0 = [#] (TOP-REAL 2);
reconsider h11 = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
reconsider h1 = h11 as Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 by A2;
h11 is continuous by TOPREAL6:83;
then h1 is continuous by A2, PRE_TOPC:62;
then consider g1 being Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 such that
A3: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2)))
for r1 being real number st h1 . p = r1 holds
g1 . p = A * r1 ) & g1 is continuous ) by A2, Th33;
consider g11 being Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 such that
A4: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2)))
for r1 being real number st g1 . p = r1 holds
g11 . p = r1 + B ) & g11 is continuous ) by A3, Th34;
dom f1 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A5: dom f1 = dom g11 by A2, FUNCT_2:def 1;
for x being set st x in dom f1 holds
f1 . x = g11 . x

proof

let x be set ; :: thesis: ( x in dom f1 implies f1 . x = g11 . x )
assume A6: x in dom f1 ; :: thesis: f1 . x = g11 . x
then A7: f1 . x = proj1 . (f . x) by FUNCT_1:22;
reconsider p = x as Point of (TOP-REAL 2) by A6, FUNCT_2:def 1;
A8: f1 . x = proj1 . |[((A * (p `1 )) + B),((C * (p `2 )) + D)]| by A1, A7
.= (A * (p `1 )) + B by PSCOMP_1:128
.= (A * (proj1 . p)) + B by PSCOMP_1:def 28 ;
A * (proj1 . p) = g1 . p by A2, A3;
hence f1 . x = g11 . x by A2, A4, A8; :: thesis: verum

end;

then A9: f1 is continuous by A4, A5, FUNCT_1:9;
reconsider h11 = proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
reconsider h1 = h11 as Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 by A2;
h11 is continuous by A2, TOPREAL6:83;
then h1 is continuous by A2, PRE_TOPC:62;
then consider g1 being Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 such that
A10: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2)))
for r1 being real number st h1 . p = r1 holds
g1 . p = C * r1 ) & g1 is continuous ) by Th33;
consider g11 being Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 such that
A11: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2)))
for r1 being real number st g1 . p = r1 holds
g11 . p = r1 + D ) & g11 is continuous ) by A10, Th34;
dom f2 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A12: dom f2 = dom g11 by A2, FUNCT_2:def 1;
for x being set st x in dom f2 holds
f2 . x = g11 . x

proof

let x be set ; :: thesis: ( x in dom f2 implies f2 . x = g11 . x )
assume A13: x in dom f2 ; :: thesis: f2 . x = g11 . x
then A14: f2 . x = proj2 . (f . x) by FUNCT_1:22;
reconsider p = x as Point of (TOP-REAL 2) by A13, FUNCT_2:def 1;
A15: f2 . x = proj2 . |[((A * (p `1 )) + B),((C * (p `2 )) + D)]| by A1, A14
.= (C * (p `2 )) + D by PSCOMP_1:128
.= (C * (proj2 . p)) + D by PSCOMP_1:def 29 ;
C * (proj2 . p) = g1 . p by A2, A10;
hence f2 . x = g11 . x by A2, A11, A15; :: thesis: verum

end;

then A16: f2 is continuous by A11, A12, FUNCT_1:9;
for x, y, r, s being real number st |[x,y]| in [#] (TOP-REAL 2) & r = f1 . |[x,y]| & s = f2 . |[x,y]| holds
f0 . |[x,y]| = |[r,s]|

proof

let x, y, r, s be real number ; :: thesis: ( |[x,y]| in [#] (TOP-REAL 2) & r = f1 . |[x,y]| & s = f2 . |[x,y]| implies f0 . |[x,y]| = |[r,s]| )
assume A17: ( |[x,y]| in [#] (TOP-REAL 2) & r = f1 . |[x,y]| & s = f2 . |[x,y]| ) ; :: thesis: f0 . |[x,y]| = |[r,s]|
A18: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A19: f . |[x,y]| is Point of (TOP-REAL 2) ;
A20: proj1 . (f0 . |[x,y]|) = r by A17, A18, FUNCT_1:23;
proj2 . (f0 . |[x,y]|) = s by A17, A18, FUNCT_1:23;
hence f0 . |[x,y]| = |[r,s]| by A19, A20, Th18; :: thesis: verum

end;

then f0 is continuous by A2, A9, A16, Th45;
hence f is continuous by A2, PRE_TOPC:64; :: thesis: verum