let R be non empty right_unital doubleLoopStr ; :: thesis: for S being non empty right_complementable right-distributive right_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
for f being multiplicative Function of R,S holds
( f . (1. R) = 0. S or f . (1. R) = 1. S )
let S be non empty right_complementable right-distributive right_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for f being multiplicative Function of R,S holds
( f . (1. R) = 0. S or f . (1. R) = 1. S )
let f be multiplicative Function of R,S; :: thesis: ( f . (1. R) = 0. S or f . (1. R) = 1. S )
A: f . (1. R) = f . ((1. R) * (1. R))
.= (f . (1. R)) * (f . (1. R)) by GROUP_6:def 6 ;
B: (f . (1. R)) * ((1. S) - (f . (1. R))) = ((f . (1. R)) * (1. S)) + ((f . (1. R)) * (- (f . (1. R)))) by VECTSP_1:def 2
.= ((f . (1. R)) * (1. S)) + (- ((f . (1. R)) * (f . (1. R)))) by VECTSP_1:8
.= (f . (1. R)) - ((f . (1. R)) * (f . (1. R)))
.= 0. S by A, RLVECT_1:15 ;
now :: thesis: ( f . (1. R) <> 0. S implies f . (1. R) = 1. S )
assume C: f . (1. R) <> 0. S ; :: thesis: f . (1. R) = 1. S
thus f . (1. R) = (f . (1. R)) + (0. S)
.= (f . (1. R)) + ((1. S) + (- (f . (1. R)))) by C, B, VECTSP_2:def 1
.= ((f . (1. R)) + (- (f . (1. R)))) + (1. S) by RLVECT_1:def 3
.= (0. S) + (1. S) by RLVECT_1:5
.= 1. S ; :: thesis: verum
end;
hence ( f . (1. R) = 0. S or f . (1. R) = 1. S ) ; :: thesis: verum