set Z = EMbedding L;
defpred S1[ object , object ] means ex vv, uu being Vector of (EMbedding L) ex v, u being Vector of L st
( $1 = [vv,uu] & vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u & $2 = <;v,u;> );
A1:
for x being Element of [: the carrier of (EMbedding L), the carrier of (EMbedding L):] ex y being Element of the carrier of F_Real st S1[x,y]
proof
let x be
Element of
[: the carrier of (EMbedding L), the carrier of (EMbedding L):];
ex y being Element of the carrier of F_Real st S1[x,y]
consider vv,
uu being
object such that B1:
(
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 B1;
consider v being
Vector of
L such that B2:
vv = (MorphsZQ L) . v
by ZMODUL08:22;
consider u being
Vector of
L such that B3:
uu = (MorphsZQ L) . u
by ZMODUL08:22;
take
<;v,u;>
;
S1[x,<;v,u;>]
thus
S1[
x,
<;v,u;>]
by B1, B2, B3;
verum
end;
consider f being Function of [: the carrier of (EMbedding L), the carrier of (EMbedding L):], the carrier of F_Real such that
A2:
for x being Element of [: the carrier of (EMbedding L), the carrier of (EMbedding L):] holds S1[x,f . x]
from FUNCT_2:sch 3(A1);
take
f
; 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
f . (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
f . (vv,uu) = <;v,u;>
proof
let v,
u be
Vector of
L;
for vv, uu being Vector of (EMbedding L) st vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u holds
f . (vv,uu) = <;v,u;>let vv,
uu be
Vector of
(EMbedding L);
( vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u implies f . (vv,uu) = <;v,u;> )
assume B1:
(
vv = (MorphsZQ L) . v &
uu = (MorphsZQ L) . u )
;
f . (vv,uu) = <;v,u;>
consider vv1,
uu1 being
Vector of
(EMbedding L),
v1,
u1 being
Vector of
L such that B2:
(
[vv1,uu1] = [vv,uu] &
vv1 = (MorphsZQ L) . v1 &
uu1 = (MorphsZQ L) . u1 &
f . (
vv,
uu)
= <;v1,u1;> )
by A2;
B3:
MorphsZQ L is
one-to-one
by ZMODUL04:def 6;
vv = (MorphsZQ L) . v1
by B2, XTUPLE_0:1;
then B4:
v1 = v
by B1, B3, FUNCT_2:19;
uu = (MorphsZQ L) . u1
by B2, XTUPLE_0:1;
hence
f . (
vv,
uu)
= <;v,u;>
by B1, B2, B3, B4, FUNCT_2:19;
verum
end;
hence
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
f . (vv,uu) = <;v,u;>
; verum