let K be non empty right_zeroed addLoopStr ; :: thesis: for V, W being non empty VectSpStr of 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 VectSpStr of 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 Th27
.= ((f . v,y) + (f . v,z)) + (f . w,(y + z)) by Th28
.= ((f . v,y) + (f . v,z)) + ((f . w,y) + (f . w,z)) by Th28 ; :: thesis: verum