defpred S₁[ object , object ] means for t being Point of (TOP-REAL 2) st t = $1 holds
$2 = |[((A * (t `1)) + B),((C * (t `2)) + D)]|;
A1: for x being object st x in the carrier of (TOP-REAL 2) holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in the carrier of (TOP-REAL 2) implies ex y being object st S₁[x,y] )
assume x in the carrier of (TOP-REAL 2) ; :: thesis: ex y being object st S₁[x,y]
then reconsider t2 = x as Point of (TOP-REAL 2) ;
reconsider y2 = |[((A * (t2 `1)) + B),((C * (t2 `2)) + D)]| as set ;
for t being Point of (TOP-REAL 2) st t = x holds
y2 = |[((A * (t `1)) + B),((C * (t `2)) + D)]| ;
hence ex y being object st S₁[x,y] ; :: thesis: verum

end;

ex ff being Function st
( dom ff = the carrier of (TOP-REAL 2) & ( for x being object st x in the carrier of (TOP-REAL 2) holds
S₁[x,ff . x] ) ) from CLASSES1:sch 1(A1);
then consider ff being Function such that
A2: dom ff = the carrier of (TOP-REAL 2) and
A3: for x being object st x in the carrier of (TOP-REAL 2) holds
for t being Point of (TOP-REAL 2) st t = x holds
ff . x = |[((A * (t `1)) + B),((C * (t `2)) + D)]| ;
for x being object st x in the carrier of (TOP-REAL 2) holds
ff . x in the carrier of (TOP-REAL 2)

proof

let x be object ; :: thesis: ( x in the carrier of (TOP-REAL 2) implies ff . x in the carrier of (TOP-REAL 2) )
assume x in the carrier of (TOP-REAL 2) ; :: thesis: ff . x in the carrier of (TOP-REAL 2)
then reconsider t = x as Point of (TOP-REAL 2) ;
ff . t = |[((A * (t `1)) + B),((C * (t `2)) + D)]| by A3;
hence ff . x in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;

then reconsider ff = ff as Function of (TOP-REAL 2),(TOP-REAL 2) by A2, FUNCT_2:3;
take ff ; :: thesis: for t being Point of (TOP-REAL 2) holds ff . t = |[((A * (t `1)) + B),((C * (t `2)) + D)]|
thus for t being Point of (TOP-REAL 2) holds ff . t = |[((A * (t `1)) + B),((C * (t `2)) + D)]| by A3; :: thesis: verum