let X be set ; :: thesis: for x being Element of holds (1_ Z_2 ) * x = x
let x be Element of ; :: thesis: (1_ Z_2 ) * x = x
reconsider c = x as Subset of ;
(1_ Z_2 ) * x = (1_ Z_2 ) \*\ c by Def6
.= c by Def4 ;
hence (1_ Z_2 ) * x = x ; :: thesis: verum