let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for V, W being VectSp of K
for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of K
for f being bilinear-Form 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 VectSp of K; :: thesis: for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of K
for f being bilinear-Form 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; :: thesis: for w, t being Vector of W
for a, b being Element of K
for f being bilinear-Form 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; :: thesis: for a, b being Element of K
for f being bilinear-Form 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 K; :: thesis: for f being bilinear-Form 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-Form of V,W; :: thesis: 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 Th37
.= ((f . (v,y)) - (b * (f . (v,z)))) - ((f . ((a * w),y)) - (f . ((a * w),(b * z)))) by Th32
.= ((f . (v,y)) - (b * (f . (v,z)))) - ((a * (f . (w,y))) - (f . ((a * w),(b * z)))) by Th31
.= ((f . (v,y)) - (b * (f . (v,z)))) - ((a * (f . (w,y))) - (a * (f . (w,(b * z))))) by Th31
.= ((f . (v,y)) - (b * (f . (v,z)))) - ((a * (f . (w,y))) - (a * (b * (f . (w,z))))) by Th32 ; :: thesis: verum