let x, y be Element of (INT.Group 2); :: thesis: ( ( x = 0 implies x * y = y ) & ( y = 0 implies x * y = x ) & ( x = 1 & y = 1 implies x * y = 1_ (INT.Group 2) ) )
thus ( x = 0 implies x * y = y ) :: thesis: ( ( y = 0 implies x * y = x ) & ( x = 1 & y = 1 implies x * y = 1_ (INT.Group 2) ) )

proof

assume x = 0 ; :: thesis: x * y = y
then x = 1_ (INT.Group 2) by GR_CY_1:14;
hence x * y = y by GROUP_1:def 4; :: thesis: verum

end;

thus ( y = 0 implies x * y = x ) :: thesis: ( x = 1 & y = 1 implies x * y = 1_ (INT.Group 2) )

proof

assume y = 0 ; :: thesis: x * y = x
then y = 1_ (INT.Group 2) by GR_CY_1:14;
hence x * y = x by GROUP_1:def 4; :: thesis: verum

end;

assume ( x = 1 & y = 1 ) ; :: thesis: x * y = 1_ (INT.Group 2)
hence x * y = 1_ (INT.Group 2) by Th82; :: thesis: verum