let K be non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis: for V, W being non empty right_complementable add-associative right_zeroed VectSp-like VectSpStr 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 non empty right_complementable add-associative right_zeroed VectSp-like VectSpStr 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 Th29
.= ((f . v,y) + (b * (f . v,z))) + ((f . (a * w),y) + (f . (a * w),(b * z))) by Th33
.= ((f . v,y) + (b * (f . v,z))) + ((a * (f . w,y)) + (f . (a * w),(b * z))) by Th32
.= ((f . v,y) + (b * (f . v,z))) + ((a * (f . w,y)) + (a * (f . w,(b * z)))) by Th32
.= ((f . v,y) + (b * (f . v,z))) + ((a * (f . w,y)) + (a * (b * (f . w,z)))) by Th33 ; :: thesis: verum