let V, W be Z_Module; :: thesis: for v, u being Vector of V
for w, t being Vector of W
for f being bilinear-FrForm of V,W holds f . ((v - u),(w - t)) = ((f . (v,w)) - (f . (v,t))) - ((f . (u,w)) - (f . (u,t)))
let v, w be Vector of V; :: thesis: for w, t being Vector of W
for f being bilinear-FrForm of V,W holds f . ((v - w),(w - t)) = ((f . (v,w)) - (f . (v,t))) - ((f . (w,w)) - (f . (w,t)))
let y, z be Vector of W; :: thesis: for f being bilinear-FrForm of V,W holds f . ((v - w),(y - z)) = ((f . (v,y)) - (f . (v,z))) - ((f . (w,y)) - (f . (w,z)))
let f be bilinear-FrForm of V,W; :: thesis: f . ((v - w),(y - z)) = ((f . (v,y)) - (f . (v,z))) - ((f . (w,y)) - (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 - w),(y - z)) = (f . (v,(y - z))) - (f . (w,(y - z))) by HTh35
.= ((f . (v,y)) - (f . (v,z))) - (f . (w,(y - z))) by HTh36
.= ((f . (v,y)) - (f . (v,z))) - ((f . (w,y)) - (f . (w,z))) by HTh36 ; :: thesis: verum