set Z = EMbedding L;
defpred S1[ object , object ] means ex vv, uu being Vector of () ex v, u being Vector of L st
( \$1 = [vv,uu] & vv = () . v & uu = () . u & \$2 = <;v,u;> );
A1: for x being Element of [: the carrier of (), the carrier of ():] ex y being Element of the carrier of F_Real st S1[x,y]
proof
let x be Element of [: the carrier of (), the carrier of ():]; :: thesis: ex y being Element of the carrier of F_Real st S1[x,y]
consider vv, uu being object such that
B1: ( vv in the carrier of () & uu in the carrier of () & x = [vv,uu] ) by ZFMISC_1:def 2;
reconsider vv = vv, uu = uu as Vector of () by B1;
consider v being Vector of L such that
B2: vv = () . v by ZMODUL08:22;
consider u being Vector of L such that
B3: uu = () . u by ZMODUL08:22;
take <;v,u;> ; :: thesis: S1[x,<;v,u;>]
thus S1[x,<;v,u;>] by B1, B2, B3; :: thesis: verum
end;
consider f being Function of [: the carrier of (), the carrier of ():], the carrier of F_Real such that
A2: for x being Element of [: the carrier of (), the carrier of ():] holds S1[x,f . x] from take f ; :: thesis: for v, u being Vector of L
for vv, uu being Vector of () st vv = () . v & uu = () . u holds
f . (vv,uu) = <;v,u;>

for v, u being Vector of L
for vv, uu being Vector of () st vv = () . v & uu = () . u holds
f . (vv,uu) = <;v,u;>
proof
let v, u be Vector of L; :: thesis: for vv, uu being Vector of () st vv = () . v & uu = () . u holds
f . (vv,uu) = <;v,u;>

let vv, uu be Vector of (); :: thesis: ( vv = () . v & uu = () . u implies f . (vv,uu) = <;v,u;> )
assume B1: ( vv = () . v & uu = () . u ) ; :: thesis: f . (vv,uu) = <;v,u;>
consider vv1, uu1 being Vector of (), v1, u1 being Vector of L such that
B2: ( [vv1,uu1] = [vv,uu] & vv1 = () . v1 & uu1 = () . u1 & f . (vv,uu) = <;v1,u1;> ) by A2;
B3: MorphsZQ L is one-to-one by ZMODUL04:def 6;
vv = () . v1 by ;
then B4: v1 = v by ;
uu = () . u1 by ;
hence f . (vv,uu) = <;v,u;> by ; :: thesis: verum
end;
hence for v, u being Vector of L
for vv, uu being Vector of () st vv = () . v & uu = () . u holds
f . (vv,uu) = <;v,u;> ; :: thesis: verum