let K be non empty right_complementable add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for V, W being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over 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 vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over 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 Th28

.= ((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

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 vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over 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 Th28

.= ((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