defpred S1[ object , object ] means ex q being Point of () st
( q = \$1 & \$2 = |(p,q)| );
A1: for x being object st x in the carrier of () holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in the carrier of () implies ex y being object st S1[x,y] )
assume x in the carrier of () ; :: thesis: ex y being object st S1[x,y]
then reconsider q3 = x as Point of () ;
take |(p,q3)| ; :: thesis: S1[x,|(p,q3)|]
thus S1[x,|(p,q3)|] ; :: thesis: verum
end;
consider f1 being Function such that
A2: ( dom f1 = the carrier of () & ( for x being object st x in the carrier of () holds
S1[x,f1 . x] ) ) from rng f1 c= the carrier of R^1
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f1 or z in the carrier of R^1 )
assume z in rng f1 ; :: thesis: z in the carrier of R^1
then consider xz being object such that
A3: xz in dom f1 and
A4: z = f1 . xz by FUNCT_1:def 3;
ex q4 being Point of () st
( q4 = xz & f1 . xz = |(p,q4)| ) by A2, A3;
hence z in the carrier of R^1 by ; :: thesis: verum
end;
then reconsider f2 = f1 as Function of (),R^1 by ;
take f2 ; :: thesis: for q being Point of () holds f2 . q = |(p,q)|
for q being Point of () holds f1 . q = |(p,q)|
proof
let q be Point of (); :: thesis: f1 . q = |(p,q)|
ex q2 being Point of () st
( q2 = q & f1 . q = |(p,q2)| ) by A2;
hence f1 . q = |(p,q)| ; :: thesis: verum
end;
hence for q being Point of () holds f2 . q = |(p,q)| ; :: thesis: verum