let f1, f2 be Function of [: the carrier of (EMbedding L), the carrier of (EMbedding L):], the carrier of F_Real; ( ( 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
f1 . (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
f2 . (vv,uu) = <;v,u;> ) implies f1 = f2 )
assume AS1:
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
f1 . (vv,uu) = <;v,u;>
; ( ex v, u being Vector of L ex vv, uu being Vector of (EMbedding L) st
( vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u & not f2 . (vv,uu) = <;v,u;> ) or f1 = f2 )
assume AS2:
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
f2 . (vv,uu) = <;v,u;>
; f1 = f2
for x being Element of [: the carrier of (EMbedding L), the carrier of (EMbedding L):] holds f1 . x = f2 . x
proof
let x be
Element of
[: the carrier of (EMbedding L), the carrier of (EMbedding L):];
f1 . x = f2 . x
consider vv,
uu being
object such that B0:
(
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 B0;
consider v being
Vector of
L such that B2:
(MorphsZQ L) . v = vv
by ZMODUL08:22;
consider u being
Vector of
L such that B3:
(MorphsZQ L) . u = uu
by ZMODUL08:22;
thus f1 . x =
f1 . (
vv,
uu)
by B0
.=
<;v,u;>
by AS1, B2, B3
.=
f2 . (
vv,
uu)
by AS2, B2, B3
.=
f2 . x
by B0
;
verum
end;
hence
f1 = f2
; verum