let V, W be non empty ModuleStr over F_Complex ; for f being Form of V,W
for a being Element of F_Complex holds (a * f) *' = (a *') * (f *')
let f be Form of V,W; for a being Element of F_Complex holds (a * f) *' = (a *') * (f *')
let a be Element of F_Complex; (a * f) *' = (a *') * (f *')
now for v being Vector of V
for w being Vector of W holds ((a * f) *') . (v,w) = ((a *') * (f *')) . (v,w)let v be
Vector of
V;
for w being Vector of W holds ((a * f) *') . (v,w) = ((a *') * (f *')) . (v,w)let w be
Vector of
W;
((a * f) *') . (v,w) = ((a *') * (f *')) . (v,w)thus ((a * f) *') . (
v,
w) =
((a * f) . (v,w)) *'
by Def8
.=
(a * (f . (v,w))) *'
by BILINEAR:def 3
.=
(a *') * ((f . (v,w)) *')
by COMPLFLD:54
.=
(a *') * ((f *') . (v,w))
by Def8
.=
((a *') * (f *')) . (
v,
w)
by BILINEAR:def 3
;
verum end;
hence
(a * f) *' = (a *') * (f *')
; verum