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

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

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;> ; :: thesis: ( 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;> ; :: thesis: f1 = f2

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

proof

hence
f1 = f2
; :: thesis: verum
let x be Element of [: the carrier of (EMbedding L), the carrier of (EMbedding L):]; :: thesis: 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 ; :: thesis: verum

end;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 ; :: thesis: verum