let G be Group; :: thesis: for g being Element of
for H being Subgroup of G
for h being Element of st h = g holds
h " = g "
let g be Element of ; :: thesis: for H being Subgroup of G
for h being Element of st h = g holds
h " = g "
let H be Subgroup of G; :: thesis: for h being Element of st h = g holds
h " = g "
let h be Element of ; :: thesis: ( h = g implies h " = g " )
reconsider g' = h " as Element of by Th51;
A1: h * (h " ) = 1_ H by GROUP_1:def 6;
assume h = g ; :: thesis: h " = g "
then g * g' = 1_ H by A1, Th52
.= 1_ G by Th53 ;
hence h " = g " by GROUP_1:20; :: thesis: verum