set Z = EMbedding L;

set D = DivisibleMod L;

let f1, f2 be Function of [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):],F_Real; :: 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

f1 . (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

f2 . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) ) implies f1 = f2 )

assume AS1: 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

f1 . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) ; :: thesis: ( 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 F_Real st

( a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu & not f2 . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) ) or f1 = f2 )

assume AS2: 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

f2 . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) ; :: thesis: f1 = f2

for x being Element of [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):] holds f1 . x = f2 . x

set D = DivisibleMod L;

let f1, f2 be Function of [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):],F_Real; :: 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

f1 . (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

f2 . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) ) implies f1 = f2 )

assume AS1: 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

f1 . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) ; :: thesis: ( 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 F_Real st

( a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu & not f2 . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) ) or f1 = f2 )

assume AS2: 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

f2 . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) ; :: thesis: f1 = f2

for x being Element of [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):] holds f1 . x = f2 . x

proof

hence
f1 = f2
; :: thesis: verum
let x be Element of [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):]; :: thesis: f1 . x = f2 . x

consider vv, uu being object such that

B0: ( 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 B0;

consider a being Element of INT.Ring such that

B1: ( a <> 0 & a * vv in EMbedding L ) by ZMODUL08:29;

consider b being Element of INT.Ring such that

B2: ( b <> 0 & b * uu in EMbedding L ) by ZMODUL08:29;

reconsider v = a * vv as Vector of (EMbedding L) by B1;

reconsider u = b * uu as Vector of (EMbedding L) by B2;

INT c= the carrier of F_Real by NUMBERS:5;

then reconsider ai = a, bi = b as Element of F_Real ;

thus f1 . x = f1 . (vv,uu) by B0

.= ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) by AS1, B1, B2

.= f2 . (vv,uu) by AS2, B1, B2

.= f2 . x by B0 ; :: thesis: verum

end;consider vv, uu being object such that

B0: ( 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 B0;

consider a being Element of INT.Ring such that

B1: ( a <> 0 & a * vv in EMbedding L ) by ZMODUL08:29;

consider b being Element of INT.Ring such that

B2: ( b <> 0 & b * uu in EMbedding L ) by ZMODUL08:29;

reconsider v = a * vv as Vector of (EMbedding L) by B1;

reconsider u = b * uu as Vector of (EMbedding L) by B2;

INT c= the carrier of F_Real by NUMBERS:5;

then reconsider ai = a, bi = b as Element of F_Real ;

thus f1 . x = f1 . (vv,uu) by B0

.= ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) by AS1, B1, B2

.= f2 . (vv,uu) by AS2, B1, B2

.= f2 . x by B0 ; :: thesis: verum