set f = InnerProduct L;
for v being Vector of L holds (curry' (InnerProduct L)) . v is additive
proof
let v be
Vector of
L;
(curry' (InnerProduct L)) . v is additive
set g =
(curry' (InnerProduct L)) . v;
for
w1,
w2 being
Vector of
L holds
((curry' (InnerProduct L)) . v) . (w1 + w2) = (((curry' (InnerProduct L)) . v) . w1) + (((curry' (InnerProduct L)) . v) . w2)
proof
let w1,
w2 be
Vector of
L;
((curry' (InnerProduct L)) . v) . (w1 + w2) = (((curry' (InnerProduct L)) . v) . w1) + (((curry' (InnerProduct L)) . v) . w2)
thus ((curry' (InnerProduct L)) . v) . (w1 + w2) =
(InnerProduct L) . (
(w1 + w2),
v)
by FUNCT_5:70
.=
<;(w1 + w2),v;>
.=
<;v,(w1 + w2);>
by defZLattice
.=
<;v,w1;> + <;v,w2;>
by ThSc2
.=
<;w1,v;> + <;v,w2;>
by defZLattice
.=
<;w1,v;> + <;w2,v;>
by defZLattice
.=
((InnerProduct L) . (w1,v)) + ((InnerProduct L) . (w2,v))
.=
(((curry' (InnerProduct L)) . v) . w1) + ((InnerProduct L) . (w2,v))
by FUNCT_5:70
.=
(((curry' (InnerProduct L)) . v) . w1) + (((curry' (InnerProduct L)) . v) . w2)
by FUNCT_5:70
;
verum
end;
hence
(curry' (InnerProduct L)) . v is
additive
;
verum
end;
hence
InnerProduct L is additiveSAF
; ( InnerProduct L is homogeneousSAF & InnerProduct L is additiveFAF & InnerProduct L is homogeneousFAF )
for v being Vector of L holds (curry' (InnerProduct L)) . v is homogeneous
hence
InnerProduct L is homogeneousSAF
; ( InnerProduct L is additiveFAF & InnerProduct L is homogeneousFAF )
for v being Vector of L holds (curry (InnerProduct L)) . v is additive
hence
InnerProduct L is additiveFAF
; InnerProduct L is homogeneousFAF
for v being Vector of L holds (curry (InnerProduct L)) . v is homogeneous
hence
InnerProduct L is homogeneousFAF
; verum