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 " )
assume A1: h = g ; :: thesis: h " = g "
reconsider g' = h " as Element of G by Th51;
h * (h " ) = 1_ H by GROUP_1:def 6;
then g * g' = 1_ H by A1, Th52
.= 1_ G by Th53 ;
hence h " = g " by GROUP_1:20; :: thesis: verum