reconsider h11 = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
set K0 = [#] (TOP-REAL 2);
let A, B, C, D be Real; :: 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 )
A1: (TOP-REAL 2) | ([#] (TOP-REAL 2)) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) by TSEP_1:93;
then reconsider h1 = h11 as Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 ;
h11 is continuous by JORDAN5A:27;
then h1 is continuous by A1, PRE_TOPC:32;
then consider g1 being Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 such that
A2: for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2)))
for r1 being Real st h1 . p = r1 holds
g1 . p = A * r1 and
A3: g1 is continuous by Th23;
reconsider f1 = proj1 * f as Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 by A1, TOPMETR:17;
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 st g1 . p = r1 holds
g11 . p = r1 + B and
A5: g11 is continuous by A3, Th24;
reconsider f2 = proj2 * f as Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 by A1, TOPMETR:17;
reconsider h11 = proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
reconsider h1 = h11 as Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 by A1;
dom f1 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A6: dom f1 = dom g11 by A1, FUNCT_2:def 1;
assume A7: for t being Point of (TOP-REAL 2) holds f . t = |[((A * (t `1)) + B),((C * (t `2)) + D)]| ; :: thesis: f is continuous
A8: for x being object st x in dom f1 holds
f1 . x = g11 . x

proof

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

end;

h11 is continuous by JORDAN5A:27;
then h1 is continuous by A1, PRE_TOPC:32;
then consider g1 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 st h1 . p = r1 holds
g1 . p = C * r1 and
A12: g1 is continuous by Th23;
consider g11 being Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 such that
A13: for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2)))
for r1 being Real st g1 . p = r1 holds
g11 . p = r1 + D and
A14: g11 is continuous by A12, Th24;
A15: for x being object st x in dom f2 holds
f2 . x = g11 . x

proof

let x be object ; :: thesis: ( x in dom f2 implies f2 . x = g11 . x )
assume A16: x in dom f2 ; :: thesis: f2 . x = g11 . x
then reconsider p = x as Point of (TOP-REAL 2) by FUNCT_2:def 1;
f2 . x = proj2 . (f . x) by A16, FUNCT_1:12;
then A17: f2 . x = proj2 . |[((A * (p `1)) + B),((C * (p `2)) + D)]| by A7
.= (C * (p `2)) + D by PSCOMP_1:65
.= (C * (proj2 . p)) + D by PSCOMP_1:def 6 ;
C * (proj2 . p) = g1 . p by A1, A11;
hence f2 . x = g11 . x by A1, A13, A17; :: thesis: verum

end;

reconsider f0 = f as Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),((TOP-REAL 2) | ([#] (TOP-REAL 2))) by A1;
A18: for x, y, r, s being Real 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; :: thesis: ( |[x,y]| in [#] (TOP-REAL 2) & r = f1 . |[x,y]| & s = f2 . |[x,y]| implies f0 . |[x,y]| = |[r,s]| )
assume that
|[x,y]| in [#] (TOP-REAL 2) and
A19: ( r = f1 . |[x,y]| & s = f2 . |[x,y]| ) ; :: thesis: f0 . |[x,y]| = |[r,s]|
A20: f . |[x,y]| is Point of (TOP-REAL 2) ;
dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then ( proj1 . (f0 . |[x,y]|) = r & proj2 . (f0 . |[x,y]|) = s ) by A19, FUNCT_1:13;
hence f0 . |[x,y]| = |[r,s]| by A20, Th8; :: thesis: verum

end;

dom f2 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then dom f2 = dom g11 by A1, FUNCT_2:def 1;
then A21: f2 is continuous by A14, A15, FUNCT_1:2;
f1 is continuous by A5, A6, A8, FUNCT_1:2;
then f0 is continuous by A21, A18, Th35;
hence f is continuous by A1, PRE_TOPC:34; :: thesis: verum