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; ( ( 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))
; ( 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))
; f1 = f2
for x being Element of [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):] holds f1 . x = f2 . x
proof
let x be
Element of
[: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):];
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
;
verum
end;
hence
f1 = f2
; verum