let K be non empty right_zeroed addLoopStr ; :: thesis: for V, W being non empty ModuleStr over K

for v, u being Vector of V

for w, t being Vector of W

for f being additiveFAF additiveSAF Form 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 non empty ModuleStr over K; :: thesis: for v, u being Vector of V

for w, t being Vector of W

for f being additiveFAF additiveSAF Form 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 additiveFAF additiveSAF Form 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 additiveFAF additiveSAF Form of V,W holds f . ((v + w),(y + z)) = ((f . (v,y)) + (f . (v,z))) + ((f . (w,y)) + (f . (w,z)))

let f be additiveFAF additiveSAF Form 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 Th26

.= ((f . (v,y)) + (f . (v,z))) + (f . (w,(y + z))) by Th27

.= ((f . (v,y)) + (f . (v,z))) + ((f . (w,y)) + (f . (w,z))) by Th27 ; :: thesis: verum

for v, u being Vector of V

for w, t being Vector of W

for f being additiveFAF additiveSAF Form 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 non empty ModuleStr over K; :: thesis: for v, u being Vector of V

for w, t being Vector of W

for f being additiveFAF additiveSAF Form 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 additiveFAF additiveSAF Form 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 additiveFAF additiveSAF Form of V,W holds f . ((v + w),(y + z)) = ((f . (v,y)) + (f . (v,z))) + ((f . (w,y)) + (f . (w,z)))

let f be additiveFAF additiveSAF Form 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 Th26

.= ((f . (v,y)) + (f . (v,z))) + (f . (w,(y + z))) by Th27

.= ((f . (v,y)) + (f . (v,z))) + ((f . (w,y)) + (f . (w,z))) by Th27 ; :: thesis: verum