let V, W be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ModuleStr over INT.Ring ; for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of INT.Ring
for f being bilinear-FrForm of V,W holds f . ((v + (a * u)),(w + (b * t))) = ((f . (v,w)) + (b * (f . (v,t)))) + ((a * (f . (u,w))) + (a * (b * (f . (u,t)))))
let v, w be Vector of V; for w, t being Vector of W
for a, b being Element of INT.Ring
for f being bilinear-FrForm of V,W holds f . ((v + (a * w)),(w + (b * t))) = ((f . (v,w)) + (b * (f . (v,t)))) + ((a * (f . (w,w))) + (a * (b * (f . (w,t)))))
let y, z be Vector of W; for a, b being Element of INT.Ring
for f being bilinear-FrForm of V,W holds f . ((v + (a * w)),(y + (b * z))) = ((f . (v,y)) + (b * (f . (v,z)))) + ((a * (f . (w,y))) + (a * (b * (f . (w,z)))))
let a, b be Element of INT.Ring; for f being bilinear-FrForm of V,W holds f . ((v + (a * w)),(y + (b * z))) = ((f . (v,y)) + (b * (f . (v,z)))) + ((a * (f . (w,y))) + (a * (b * (f . (w,z)))))
let f be bilinear-FrForm of V,W; f . ((v + (a * w)),(y + (b * z))) = ((f . (v,y)) + (b * (f . (v,z)))) + ((a * (f . (w,y))) + (a * (b * (f . (w,z)))))
set v1 = f . (v,y);
set v3 = f . (v,z);
set v4 = f . (w,y);
set v5 = f . (w,z);
thus f . ((v + (a * w)),(y + (b * z))) =
((f . (v,y)) + (f . (v,(b * z)))) + ((f . ((a * w),y)) + (f . ((a * w),(b * z))))
by HTh28
.=
((f . (v,y)) + (b * (f . (v,z)))) + ((f . ((a * w),y)) + (f . ((a * w),(b * z))))
by HTh32
.=
((f . (v,y)) + (b * (f . (v,z)))) + ((a * (f . (w,y))) + (f . ((a * w),(b * z))))
by HTh31
.=
((f . (v,y)) + (b * (f . (v,z)))) + ((a * (f . (w,y))) + (a * (f . (w,(b * z)))))
by HTh31
.=
((f . (v,y)) + (b * (f . (v,z)))) + ((a * (f . (w,y))) + (a * (b * (f . (w,z)))))
by HTh32
; verum