set Z = EMbedding L;

defpred S_{1}[ object , object ] means ex vv, uu being Vector of (EMbedding L) ex v, u being Vector of L st

( $1 = [vv,uu] & vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u & $2 = <;v,u;> );

A1: for x being Element of [: the carrier of (EMbedding L), the carrier of (EMbedding L):] ex y being Element of the carrier of F_Real st S_{1}[x,y]

A2: for x being Element of [: the carrier of (EMbedding L), the carrier of (EMbedding L):] holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A1);

take f ; :: thesis: for v, u being Vector of L

for vv, uu being Vector of (EMbedding L) st vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u holds

f . (vv,uu) = <;v,u;>

for v, u being Vector of L

for vv, uu being Vector of (EMbedding L) st vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u holds

f . (vv,uu) = <;v,u;>

for vv, uu being Vector of (EMbedding L) st vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u holds

f . (vv,uu) = <;v,u;> ; :: thesis: verum

defpred S

( $1 = [vv,uu] & vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u & $2 = <;v,u;> );

A1: for x being Element of [: the carrier of (EMbedding L), the carrier of (EMbedding L):] ex y being Element of the carrier of F_Real st S

proof

consider f being Function of [: the carrier of (EMbedding L), the carrier of (EMbedding L):], the carrier of F_Real such that
let x be Element of [: the carrier of (EMbedding L), the carrier of (EMbedding L):]; :: thesis: ex y being Element of the carrier of F_Real st S_{1}[x,y]

consider vv, uu being object such that

B1: ( vv in the carrier of (EMbedding L) & uu in the carrier of (EMbedding L) & x = [vv,uu] ) by ZFMISC_1:def 2;

reconsider vv = vv, uu = uu as Vector of (EMbedding L) by B1;

consider v being Vector of L such that

B2: vv = (MorphsZQ L) . v by ZMODUL08:22;

consider u being Vector of L such that

B3: uu = (MorphsZQ L) . u by ZMODUL08:22;

take <;v,u;> ; :: thesis: S_{1}[x,<;v,u;>]

thus S_{1}[x,<;v,u;>]
by B1, B2, B3; :: thesis: verum

end;consider vv, uu being object such that

B1: ( vv in the carrier of (EMbedding L) & uu in the carrier of (EMbedding L) & x = [vv,uu] ) by ZFMISC_1:def 2;

reconsider vv = vv, uu = uu as Vector of (EMbedding L) by B1;

consider v being Vector of L such that

B2: vv = (MorphsZQ L) . v by ZMODUL08:22;

consider u being Vector of L such that

B3: uu = (MorphsZQ L) . u by ZMODUL08:22;

take <;v,u;> ; :: thesis: S

thus S

A2: for x being Element of [: the carrier of (EMbedding L), the carrier of (EMbedding L):] holds S

take f ; :: thesis: for v, u being Vector of L

for vv, uu being Vector of (EMbedding L) st vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u holds

f . (vv,uu) = <;v,u;>

for v, u being Vector of L

for vv, uu being Vector of (EMbedding L) st vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u holds

f . (vv,uu) = <;v,u;>

proof

hence
for v, u being Vector of L
let v, u be Vector of L; :: thesis: for vv, uu being Vector of (EMbedding L) st vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u holds

f . (vv,uu) = <;v,u;>

let vv, uu be Vector of (EMbedding L); :: thesis: ( vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u implies f . (vv,uu) = <;v,u;> )

assume B1: ( vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u ) ; :: thesis: f . (vv,uu) = <;v,u;>

consider vv1, uu1 being Vector of (EMbedding L), v1, u1 being Vector of L such that

B2: ( [vv1,uu1] = [vv,uu] & vv1 = (MorphsZQ L) . v1 & uu1 = (MorphsZQ L) . u1 & f . (vv,uu) = <;v1,u1;> ) by A2;

B3: MorphsZQ L is one-to-one by ZMODUL04:def 6;

vv = (MorphsZQ L) . v1 by B2, XTUPLE_0:1;

then B4: v1 = v by B1, B3, FUNCT_2:19;

uu = (MorphsZQ L) . u1 by B2, XTUPLE_0:1;

hence f . (vv,uu) = <;v,u;> by B1, B2, B3, B4, FUNCT_2:19; :: thesis: verum

end;f . (vv,uu) = <;v,u;>

let vv, uu be Vector of (EMbedding L); :: thesis: ( vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u implies f . (vv,uu) = <;v,u;> )

assume B1: ( vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u ) ; :: thesis: f . (vv,uu) = <;v,u;>

consider vv1, uu1 being Vector of (EMbedding L), v1, u1 being Vector of L such that

B2: ( [vv1,uu1] = [vv,uu] & vv1 = (MorphsZQ L) . v1 & uu1 = (MorphsZQ L) . u1 & f . (vv,uu) = <;v1,u1;> ) by A2;

B3: MorphsZQ L is one-to-one by ZMODUL04:def 6;

vv = (MorphsZQ L) . v1 by B2, XTUPLE_0:1;

then B4: v1 = v by B1, B3, FUNCT_2:19;

uu = (MorphsZQ L) . u1 by B2, XTUPLE_0:1;

hence f . (vv,uu) = <;v,u;> by B1, B2, B3, B4, FUNCT_2:19; :: thesis: verum

for vv, uu being Vector of (EMbedding L) st vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u holds

f . (vv,uu) = <;v,u;> ; :: thesis: verum