let V be non empty right_zeroed addLoopStr ; :: thesis: for W being non empty right_complementable add-associative right_zeroed addLoopStr
for h being Function of the carrier of V, the carrier of W st h is additive holds
h . (0. V) = 0. W
let W be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for h being Function of the carrier of V, the carrier of W st h is additive holds
h . (0. V) = 0. W
let h be Function of the carrier of V, the carrier of W; :: thesis: ( h is additive implies h . (0. V) = 0. W )
set z = 0. V;
assume A1: h is additive ; :: thesis: h . (0. V) = 0. W
h . (0. V) = h . ((0. V) + (0. V)) by RLVECT_1:def 4
.= (h . (0. V)) + (h . (0. V)) by A1 ;
hence h . (0. V) = 0. W by RLVECT_1:9; :: thesis: verum