let G be Group; :: thesis: for g being Element of G
for H being Subgroup of G
for h being Element of H st h = g holds
h " = g "
let g be Element of G; :: thesis: for H being Subgroup of G
for h being Element of H st h = g holds
h " = g "
let H be Subgroup of G; :: thesis: for h being Element of H st h = g holds
h " = g "
let h be Element of H; :: thesis: ( h = g implies h " = g " )
reconsider g9 = h " as Element of G by Th42;
A1: h * (h ") = 1_ H by GROUP_1:def 5;
assume h = g ; :: thesis: h " = g "
then g * g9 = 1_ H by A1, Th43
.= 1_ G by Th44 ;
hence h " = g " by GROUP_1:12; :: thesis: verum