set Z = EMbedding L;
set D = DivisibleMod L;
defpred S1[ object , object ] means ex vv, uu being Vector of () ex v, u being Vector of () ex a, b being Element of INT.Ring ex ai, bi being Element of INT st
( \$1 = [vv,uu] & a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu & \$2 = ((ai ") * (bi ")) * (() . (v,u)) );
A1: for x being Element of [: the carrier of (), the carrier of ():] ex y being Element 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 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 a being Element of INT.Ring such that
B2: ( a <> 0. INT.Ring & a * vv in EMbedding L ) by ZMODUL08:29;
reconsider v = a * vv as Vector of () by B2;
consider b being Element of INT.Ring such that
B3: ( b <> 0. INT.Ring & b * uu in EMbedding L ) by ZMODUL08:29;
reconsider u = b * uu as Vector of () by B3;
reconsider ai = a, bi = b as Element of INT ;
take ((ai ") * (bi ")) * (() . (v,u)) ; :: thesis: ( ((ai ") * (bi ")) * (() . (v,u)) is Element of F_Real & S1[x,((ai ") * (bi ")) * (() . (v,u))] )
thus ( ((ai ") * (bi ")) * (() . (v,u)) is Element of F_Real & S1[x,((ai ") * (bi ")) * (() . (v,u))] ) by ; :: thesis: verum
end;
consider f being Function 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 vv, uu being Vector of ()
for v, u being Vector of ()
for a, b being Element of INT.Ring
for ai, bi being Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu holds
f . (vv,uu) = ((ai ") * (bi ")) * (() . (v,u))

for vv, uu being Vector of ()
for v, u being Vector of ()
for a, b being Element of INT.Ring
for ai, bi being Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu holds
f . (vv,uu) = ((ai ") * (bi ")) * (() . (v,u))
proof
let vv, uu be Vector of (); :: thesis: for v, u being Vector of ()
for a, b being Element of INT.Ring
for ai, bi being Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu holds
f . (vv,uu) = ((ai ") * (bi ")) * (() . (v,u))

let v, u be Vector of (); :: thesis: for a, b being Element of INT.Ring
for ai, bi being Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu holds
f . (vv,uu) = ((ai ") * (bi ")) * (() . (v,u))

let a, b be Element of INT.Ring; :: thesis: for ai, bi being Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu holds
f . (vv,uu) = ((ai ") * (bi ")) * (() . (v,u))

let ai0, bi0 be Element of F_Real; :: thesis: ( a = ai0 & b = bi0 & ai0 <> 0 & bi0 <> 0 & v = a * vv & u = b * uu implies f . (vv,uu) = ((ai0 ") * (bi0 ")) * (() . (v,u)) )
assume B1: ( a = ai0 & b = bi0 & ai0 <> 0 & bi0 <> 0 & v = a * vv & u = b * uu ) ; :: thesis: f . (vv,uu) = ((ai0 ") * (bi0 ")) * (() . (v,u))
reconsider ai = ai0, bi = bi0 as Element of INT by B1;
consider vv1, uu1 being Vector of (), v1, u1 being Vector of (), a1, b1 being Element of INT.Ring, a1i, b1i being Element of INT such that
B2: ( [vv1,uu1] = [vv,uu] & a1 = a1i & b1 = b1i & a1i <> 0 & b1i <> 0 & v1 = a1 * vv1 & u1 = b1 * uu1 & f . (vv,uu) = ((a1i ") * (b1i ")) * (() . (v1,u1)) ) by A2;
B3: v1 = a1 * vv by ;
B4: u1 = b1 * uu by ;
reconsider a1ga = a1i gcd ai, b1gb = b1i gcd bi as Element of INT.Ring by INT_1:def 2;
BX: EMbedding L is Submodule of DivisibleMod L by ZMODUL08:24;
B5: a1ga * vv in EMbedding L
proof
consider c10, c20 being Integer such that
C10: a1i gcd ai = (c10 * a1i) + (c20 * ai) by NAT_D:68;
reconsider c1 = c10, c2 = c20 as Element of INT.Ring by INT_1:def 2;
C2: (c1 * a1) * vv = c1 * (a1 * vv) by VECTSP_1:def 16
.= c1 * v1 by ;
C3: (c2 * a) * vv = c2 * (a * vv) by VECTSP_1:def 16
.= c2 * v by ;
a1ga * vv = ((c1 * a1) + (c2 * a)) * vv by B1, B2, C10
.= ((c1 * a1) * vv) + ((c2 * a) * vv) by VECTSP_1:def 15
.= (c1 * v1) + (c2 * v) by ;
hence a1ga * vv in EMbedding L ; :: thesis: verum
end;
consider c10, c20 being Integer such that
C10: b1i gcd bi = (c10 * b1i) + (c20 * bi) by NAT_D:68;
reconsider c1 = c10, c2 = c20 as Element of INT.Ring by INT_1:def 2;
C2: (c1 * b1) * uu = c1 * (b1 * uu) by VECTSP_1:def 16
.= c1 * u1 by ;
C3: (c2 * b) * uu = c2 * (b * uu) by VECTSP_1:def 16
.= c2 * u by ;
reconsider agv = a1ga * vv as Vector of () by B5;
b1gb * uu = ((c1 * b1) + (c2 * b)) * uu by B1, B2, C10
.= ((c1 * b1) * uu) + ((c2 * b) * uu) by VECTSP_1:def 15
.= (c1 * u1) + (c2 * u) by ;
then reconsider bgu = b1gb * uu as Vector of () ;
consider ci being Integer such that
B7: ai = (a1i gcd ai) * ci by ;
consider c1i being Integer such that
B8: a1i = (a1i gcd ai) * c1i by ;
consider di being Integer such that
B9: bi = (b1i gcd bi) * di by ;
reconsider c = ci, d = di as Element of INT.Ring by INT_1:def 2;
consider d1i being Integer such that
B10: b1i = (b1i gcd bi) * d1i by ;
reconsider c = ci, c1 = c1i, d = di, d1 = d1i as Element of INT.Ring by INT_1:def 2;
B11: v = (c * a1ga) * vv by B1, B7
.= c * (a1ga * vv) by VECTSP_1:def 16
.= c * agv by ;
B12: v1 = (c1 * a1ga) * vv by
.= c1 * (a1ga * vv) by VECTSP_1:def 16
.= c1 * agv by ;
B13: u = (d * b1gb) * uu by B1, B9
.= d * (b1gb * uu) by VECTSP_1:def 16
.= d * bgu by ;
B14: u1 = (d1 * b1gb) * uu by
.= d1 * (b1gb * uu) by VECTSP_1:def 16
.= d1 * bgu by ;
B15: ci <> 0 by B1, B7;
B16: c1i <> 0 by B2, B8;
B17: di <> 0 by B1, B9;
B18: d1i <> 0 by ;
B19: f . (vv,uu) = ((a1i ") * (b1i ")) * (c1i * (() . (agv,(d1 * bgu)))) by
.= ((a1i ") * (b1i ")) * (c1i * (() . ((d1 * bgu),agv))) by ThSPEM1
.= ((a1i ") * (b1i ")) * (c1i * (d1i * (() . (bgu,agv)))) by ThSPEM1
.= ((a1i ") * (b1i ")) * (c1i * (d1i * (() . (agv,bgu)))) by ThSPEM1
.= ((((a1i ") * (b1i ")) * c1i) * d1i) * (() . (agv,bgu))
.= ((((((a1i gcd ai) ") * (c1i ")) * (((b1i gcd bi) * d1i) ")) * c1i) * d1i) * (() . (agv,bgu)) by
.= ((((((a1i gcd ai) ") * c1i) * (c1i ")) * (((b1i gcd bi) * d1i) ")) * d1i) * (() . (agv,bgu))
.= ((((a1i gcd ai) ") * (((b1i gcd bi) * d1i) ")) * d1i) * (() . (agv,bgu)) by
.= (((((b1i gcd bi) * d1i) ") * d1i) * ((a1i gcd ai) ")) * (() . (agv,bgu))
.= (((((b1i gcd bi) ") * (d1i ")) * d1i) * ((a1i gcd ai) ")) * (() . (agv,bgu)) by XCMPLX_1:204
.= (((((b1i gcd bi) ") * d1i) * (d1i ")) * ((a1i gcd ai) ")) * (() . (agv,bgu))
.= (((b1i gcd bi) ") * ((a1i gcd ai) ")) * (() . (agv,bgu)) by ;
X1: ((ai ") * (bi ")) * (() . (v,u)) = ((ai ") * (bi ")) * (ci * (() . (agv,(d * bgu)))) by
.= ((ai ") * (bi ")) * (ci * (() . ((d * bgu),agv))) by ThSPEM1
.= ((ai ") * (bi ")) * (ci * (di * (() . (bgu,agv)))) by ThSPEM1
.= ((ai ") * (bi ")) * (ci * (di * (() . (agv,bgu)))) by ThSPEM1
.= ((((((a1i gcd ai) * ci) ") * (((b1i gcd bi) * di) ")) * ci) * di) * (() . (agv,bgu)) by B7, B9
.= ((((((a1i gcd ai) ") * (ci ")) * (((b1i gcd bi) * di) ")) * ci) * di) * (() . (agv,bgu)) by XCMPLX_1:204
.= ((((((a1i gcd ai) ") * ci) * (ci ")) * (((b1i gcd bi) * di) ")) * di) * (() . (agv,bgu))
.= ((((a1i gcd ai) ") * (((b1i gcd bi) * di) ")) * di) * (() . (agv,bgu)) by
.= (((((b1i gcd bi) * di) ") * di) * ((a1i gcd ai) ")) * (() . (agv,bgu))
.= (((((b1i gcd bi) ") * (di ")) * di) * ((a1i gcd ai) ")) * (() . (agv,bgu)) by XCMPLX_1:204
.= (((((b1i gcd bi) ") * di) * (di ")) * ((a1i gcd ai) ")) * (() . (agv,bgu))
.= (((b1i gcd bi) ") * ((a1i gcd ai) ")) * (() . (agv,bgu)) by ;
( ai " = ai0 " & bi " = bi0 " ) by ;
hence f . (vv,uu) = ((ai0 ") * (bi0 ")) * (() . (v,u)) by ; :: thesis: verum
end;
hence for vv, uu being Vector of ()
for v, u being Vector of ()
for a, b being Element of INT.Ring
for ai, bi being Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu holds
f . (vv,uu) = ((ai ") * (bi ")) * (() . (v,u)) ; :: thesis: verum