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

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