set Z = EMbedding L;

set D = DivisibleMod L;

defpred S_{1}[ object , object ] means ex vv, uu being Vector of (DivisibleMod L) ex v, u being Vector of (EMbedding L) 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 ")) * ((ScProductEM L) . (v,u)) );

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

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

take f ; :: thesis: for vv, uu being Vector of (DivisibleMod L)

for v, u being Vector of (EMbedding L)

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 ")) * ((ScProductEM L) . (v,u))

for vv, uu being Vector of (DivisibleMod L)

for v, u being Vector of (EMbedding L)

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 ")) * ((ScProductEM L) . (v,u))

for v, u being Vector of (EMbedding L)

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 ")) * ((ScProductEM L) . (v,u)) ; :: thesis: verum

set D = DivisibleMod L;

defpred S

( $1 = [vv,uu] & a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu & $2 = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) );

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

proof

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

consider vv, uu being object such that

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

reconsider vv = vv, uu = uu as Vector of (DivisibleMod L) 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 (EMbedding L) 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 (EMbedding L) by B3;

reconsider ai = a, bi = b as Element of INT ;

take ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) ; :: thesis: ( ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) is Element of F_Real & S_{1}[x,((ai ") * (bi ")) * ((ScProductEM L) . (v,u))] )

thus ( ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) is Element of F_Real & S_{1}[x,((ai ") * (bi ")) * ((ScProductEM L) . (v,u))] )
by B1, B2, B3, XREAL_0:def 1; :: thesis: verum

end;consider vv, uu being object such that

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

reconsider vv = vv, uu = uu as Vector of (DivisibleMod L) 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 (EMbedding L) 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 (EMbedding L) by B3;

reconsider ai = a, bi = b as Element of INT ;

take ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) ; :: thesis: ( ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) is Element of F_Real & S

thus ( ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) is Element of F_Real & S

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

take f ; :: thesis: for vv, uu being Vector of (DivisibleMod L)

for v, u being Vector of (EMbedding L)

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 ")) * ((ScProductEM L) . (v,u))

for vv, uu being Vector of (DivisibleMod L)

for v, u being Vector of (EMbedding L)

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 ")) * ((ScProductEM L) . (v,u))

proof

hence
for vv, uu being Vector of (DivisibleMod L)
let vv, uu be Vector of (DivisibleMod L); :: thesis: for v, u being Vector of (EMbedding L)

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 ")) * ((ScProductEM L) . (v,u))

let v, u be Vector of (EMbedding L); :: 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 ")) * ((ScProductEM L) . (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 ")) * ((ScProductEM L) . (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 ")) * ((ScProductEM L) . (v,u)) )

assume B1: ( a = ai0 & b = bi0 & ai0 <> 0 & bi0 <> 0 & v = a * vv & u = b * uu ) ; :: thesis: f . (vv,uu) = ((ai0 ") * (bi0 ")) * ((ScProductEM L) . (v,u))

reconsider ai = ai0, bi = bi0 as Element of INT by B1;

consider vv1, uu1 being Vector of (DivisibleMod L), v1, u1 being Vector of (EMbedding L), 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 ")) * ((ScProductEM L) . (v1,u1)) ) by A2;

B3: v1 = a1 * vv by B2, XTUPLE_0:1;

B4: u1 = b1 * uu by B2, XTUPLE_0:1;

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

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 B4, BX, ZMODUL01:29 ;

C3: (c2 * b) * uu = c2 * (b * uu) by VECTSP_1:def 16

.= c2 * u by B1, BX, ZMODUL01:29 ;

reconsider agv = a1ga * vv as Vector of (EMbedding L) 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 C2, C3, BX, ZMODUL01:28 ;

then reconsider bgu = b1gb * uu as Vector of (EMbedding L) ;

consider ci being Integer such that

B7: ai = (a1i gcd ai) * ci by INT_1:def 3, INT_2:21;

consider c1i being Integer such that

B8: a1i = (a1i gcd ai) * c1i by INT_1:def 3, INT_2:21;

consider di being Integer such that

B9: bi = (b1i gcd bi) * di by INT_1:def 3, INT_2:21;

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 INT_1:def 3, INT_2:21;

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 BX, ZMODUL01:29 ;

B12: v1 = (c1 * a1ga) * vv by B2, B8, XTUPLE_0:1

.= c1 * (a1ga * vv) by VECTSP_1:def 16

.= c1 * agv by BX, ZMODUL01:29 ;

B13: u = (d * b1gb) * uu by B1, B9

.= d * (b1gb * uu) by VECTSP_1:def 16

.= d * bgu by BX, ZMODUL01:29 ;

B14: u1 = (d1 * b1gb) * uu by B2, B10, XTUPLE_0:1

.= d1 * (b1gb * uu) by VECTSP_1:def 16

.= d1 * bgu by BX, ZMODUL01:29 ;

B15: ci <> 0 by B1, B7;

B16: c1i <> 0 by B2, B8;

B17: di <> 0 by B1, B9;

B18: d1i <> 0 by B2, B10;

B19: f . (vv,uu) = ((a1i ") * (b1i ")) * (c1i * ((ScProductEM L) . (agv,(d1 * bgu)))) by B2, B12, B14, ThSPEM1

.= ((a1i ") * (b1i ")) * (c1i * ((ScProductEM L) . ((d1 * bgu),agv))) by ThSPEM1

.= ((a1i ") * (b1i ")) * (c1i * (d1i * ((ScProductEM L) . (bgu,agv)))) by ThSPEM1

.= ((a1i ") * (b1i ")) * (c1i * (d1i * ((ScProductEM L) . (agv,bgu)))) by ThSPEM1

.= ((((a1i ") * (b1i ")) * c1i) * d1i) * ((ScProductEM L) . (agv,bgu))

.= ((((((a1i gcd ai) ") * (c1i ")) * (((b1i gcd bi) * d1i) ")) * c1i) * d1i) * ((ScProductEM L) . (agv,bgu)) by B8, B10, XCMPLX_1:204

.= ((((((a1i gcd ai) ") * c1i) * (c1i ")) * (((b1i gcd bi) * d1i) ")) * d1i) * ((ScProductEM L) . (agv,bgu))

.= ((((a1i gcd ai) ") * (((b1i gcd bi) * d1i) ")) * d1i) * ((ScProductEM L) . (agv,bgu)) by B16, XCMPLX_1:203

.= (((((b1i gcd bi) * d1i) ") * d1i) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu))

.= (((((b1i gcd bi) ") * (d1i ")) * d1i) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu)) by XCMPLX_1:204

.= (((((b1i gcd bi) ") * d1i) * (d1i ")) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu))

.= (((b1i gcd bi) ") * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu)) by B18, XCMPLX_1:203 ;

X1: ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) = ((ai ") * (bi ")) * (ci * ((ScProductEM L) . (agv,(d * bgu)))) by B11, B13, ThSPEM1

.= ((ai ") * (bi ")) * (ci * ((ScProductEM L) . ((d * bgu),agv))) by ThSPEM1

.= ((ai ") * (bi ")) * (ci * (di * ((ScProductEM L) . (bgu,agv)))) by ThSPEM1

.= ((ai ") * (bi ")) * (ci * (di * ((ScProductEM L) . (agv,bgu)))) by ThSPEM1

.= ((((((a1i gcd ai) * ci) ") * (((b1i gcd bi) * di) ")) * ci) * di) * ((ScProductEM L) . (agv,bgu)) by B7, B9

.= ((((((a1i gcd ai) ") * (ci ")) * (((b1i gcd bi) * di) ")) * ci) * di) * ((ScProductEM L) . (agv,bgu)) by XCMPLX_1:204

.= ((((((a1i gcd ai) ") * ci) * (ci ")) * (((b1i gcd bi) * di) ")) * di) * ((ScProductEM L) . (agv,bgu))

.= ((((a1i gcd ai) ") * (((b1i gcd bi) * di) ")) * di) * ((ScProductEM L) . (agv,bgu)) by B15, XCMPLX_1:203

.= (((((b1i gcd bi) * di) ") * di) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu))

.= (((((b1i gcd bi) ") * (di ")) * di) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu)) by XCMPLX_1:204

.= (((((b1i gcd bi) ") * di) * (di ")) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu))

.= (((b1i gcd bi) ") * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu)) by B17, XCMPLX_1:203 ;

( ai " = ai0 " & bi " = bi0 " ) by LMINTFREAL1, B1;

hence f . (vv,uu) = ((ai0 ") * (bi0 ")) * ((ScProductEM L) . (v,u)) by X1, B19; :: thesis: verum

end;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 ")) * ((ScProductEM L) . (v,u))

let v, u be Vector of (EMbedding L); :: 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 ")) * ((ScProductEM L) . (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 ")) * ((ScProductEM L) . (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 ")) * ((ScProductEM L) . (v,u)) )

assume B1: ( a = ai0 & b = bi0 & ai0 <> 0 & bi0 <> 0 & v = a * vv & u = b * uu ) ; :: thesis: f . (vv,uu) = ((ai0 ") * (bi0 ")) * ((ScProductEM L) . (v,u))

reconsider ai = ai0, bi = bi0 as Element of INT by B1;

consider vv1, uu1 being Vector of (DivisibleMod L), v1, u1 being Vector of (EMbedding L), 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 ")) * ((ScProductEM L) . (v1,u1)) ) by A2;

B3: v1 = a1 * vv by B2, XTUPLE_0:1;

B4: u1 = b1 * uu by B2, XTUPLE_0:1;

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
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 B3, BX, ZMODUL01:29 ;

C3: (c2 * a) * vv = c2 * (a * vv) by VECTSP_1:def 16

.= c2 * v by B1, BX, ZMODUL01:29 ;

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 C2, C3, BX, ZMODUL01:28 ;

hence a1ga * vv in EMbedding L ; :: thesis: verum

end;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 B3, BX, ZMODUL01:29 ;

C3: (c2 * a) * vv = c2 * (a * vv) by VECTSP_1:def 16

.= c2 * v by B1, BX, ZMODUL01:29 ;

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 C2, C3, BX, ZMODUL01:28 ;

hence a1ga * vv in EMbedding L ; :: thesis: verum

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 B4, BX, ZMODUL01:29 ;

C3: (c2 * b) * uu = c2 * (b * uu) by VECTSP_1:def 16

.= c2 * u by B1, BX, ZMODUL01:29 ;

reconsider agv = a1ga * vv as Vector of (EMbedding L) 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 C2, C3, BX, ZMODUL01:28 ;

then reconsider bgu = b1gb * uu as Vector of (EMbedding L) ;

consider ci being Integer such that

B7: ai = (a1i gcd ai) * ci by INT_1:def 3, INT_2:21;

consider c1i being Integer such that

B8: a1i = (a1i gcd ai) * c1i by INT_1:def 3, INT_2:21;

consider di being Integer such that

B9: bi = (b1i gcd bi) * di by INT_1:def 3, INT_2:21;

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 INT_1:def 3, INT_2:21;

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 BX, ZMODUL01:29 ;

B12: v1 = (c1 * a1ga) * vv by B2, B8, XTUPLE_0:1

.= c1 * (a1ga * vv) by VECTSP_1:def 16

.= c1 * agv by BX, ZMODUL01:29 ;

B13: u = (d * b1gb) * uu by B1, B9

.= d * (b1gb * uu) by VECTSP_1:def 16

.= d * bgu by BX, ZMODUL01:29 ;

B14: u1 = (d1 * b1gb) * uu by B2, B10, XTUPLE_0:1

.= d1 * (b1gb * uu) by VECTSP_1:def 16

.= d1 * bgu by BX, ZMODUL01:29 ;

B15: ci <> 0 by B1, B7;

B16: c1i <> 0 by B2, B8;

B17: di <> 0 by B1, B9;

B18: d1i <> 0 by B2, B10;

B19: f . (vv,uu) = ((a1i ") * (b1i ")) * (c1i * ((ScProductEM L) . (agv,(d1 * bgu)))) by B2, B12, B14, ThSPEM1

.= ((a1i ") * (b1i ")) * (c1i * ((ScProductEM L) . ((d1 * bgu),agv))) by ThSPEM1

.= ((a1i ") * (b1i ")) * (c1i * (d1i * ((ScProductEM L) . (bgu,agv)))) by ThSPEM1

.= ((a1i ") * (b1i ")) * (c1i * (d1i * ((ScProductEM L) . (agv,bgu)))) by ThSPEM1

.= ((((a1i ") * (b1i ")) * c1i) * d1i) * ((ScProductEM L) . (agv,bgu))

.= ((((((a1i gcd ai) ") * (c1i ")) * (((b1i gcd bi) * d1i) ")) * c1i) * d1i) * ((ScProductEM L) . (agv,bgu)) by B8, B10, XCMPLX_1:204

.= ((((((a1i gcd ai) ") * c1i) * (c1i ")) * (((b1i gcd bi) * d1i) ")) * d1i) * ((ScProductEM L) . (agv,bgu))

.= ((((a1i gcd ai) ") * (((b1i gcd bi) * d1i) ")) * d1i) * ((ScProductEM L) . (agv,bgu)) by B16, XCMPLX_1:203

.= (((((b1i gcd bi) * d1i) ") * d1i) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu))

.= (((((b1i gcd bi) ") * (d1i ")) * d1i) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu)) by XCMPLX_1:204

.= (((((b1i gcd bi) ") * d1i) * (d1i ")) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu))

.= (((b1i gcd bi) ") * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu)) by B18, XCMPLX_1:203 ;

X1: ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) = ((ai ") * (bi ")) * (ci * ((ScProductEM L) . (agv,(d * bgu)))) by B11, B13, ThSPEM1

.= ((ai ") * (bi ")) * (ci * ((ScProductEM L) . ((d * bgu),agv))) by ThSPEM1

.= ((ai ") * (bi ")) * (ci * (di * ((ScProductEM L) . (bgu,agv)))) by ThSPEM1

.= ((ai ") * (bi ")) * (ci * (di * ((ScProductEM L) . (agv,bgu)))) by ThSPEM1

.= ((((((a1i gcd ai) * ci) ") * (((b1i gcd bi) * di) ")) * ci) * di) * ((ScProductEM L) . (agv,bgu)) by B7, B9

.= ((((((a1i gcd ai) ") * (ci ")) * (((b1i gcd bi) * di) ")) * ci) * di) * ((ScProductEM L) . (agv,bgu)) by XCMPLX_1:204

.= ((((((a1i gcd ai) ") * ci) * (ci ")) * (((b1i gcd bi) * di) ")) * di) * ((ScProductEM L) . (agv,bgu))

.= ((((a1i gcd ai) ") * (((b1i gcd bi) * di) ")) * di) * ((ScProductEM L) . (agv,bgu)) by B15, XCMPLX_1:203

.= (((((b1i gcd bi) * di) ") * di) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu))

.= (((((b1i gcd bi) ") * (di ")) * di) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu)) by XCMPLX_1:204

.= (((((b1i gcd bi) ") * di) * (di ")) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu))

.= (((b1i gcd bi) ") * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu)) by B17, XCMPLX_1:203 ;

( ai " = ai0 " & bi " = bi0 " ) by LMINTFREAL1, B1;

hence f . (vv,uu) = ((ai0 ") * (bi0 ")) * ((ScProductEM L) . (v,u)) by X1, B19; :: thesis: verum

for v, u being Vector of (EMbedding L)

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 ")) * ((ScProductEM L) . (v,u)) ; :: thesis: verum