let R be non empty doubleLoopStr ; :: thesis: id R is RingHomomorphism
A1: for x, y being Element of R holds (id R) . (x + y) = ((id R) . x) + ((id R) . y)

proof

let x, y be Element of R; :: thesis: (id R) . (x + y) = ((id R) . x) + ((id R) . y)
thus ((id R) . x) + ((id R) . y) = x + ((id R) . y) by FUNCT_1:35
.= x + y by FUNCT_1:35
.= (id R) . (x + y) by FUNCT_1:35 ; :: thesis: verum

end;

A2: for x, y being Element of R holds (id R) . (x * y) = ((id R) . x) * ((id R) . y)

proof

let x, y be Element of R; :: thesis: (id R) . (x * y) = ((id R) . x) * ((id R) . y)
thus ((id R) . x) * ((id R) . y) = x * ((id R) . y) by FUNCT_1:35
.= x * y by FUNCT_1:35
.= (id R) . (x * y) by FUNCT_1:35 ; :: thesis: verum

end;

(id R) . (1_ R) = 1_ R by FUNCT_1:35;
then ( id R is additive & id R is multiplicative & id R is unity-preserving ) by A1, A2, GRCAT_1:def 13, GROUP_1:def 17, GROUP_6:def 7;
hence id R is RingHomomorphism ; :: thesis: verum