let R be non empty right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for S being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for f being additive Function of R,S holds f . (0. R) = 0. S
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for f being additive Function of R,S holds f . (0. R) = 0. S
let f be additive Function of R,S; :: thesis: f . (0. R) = 0. S
f . (0. R) = f . ((0. R) + (0. R))
.= (f . (0. R)) + (f . (0. R)) by VECTSP_1:def 20 ;
hence f . (0. R) = 0. S by RLVECT_1:9; :: thesis: verum