let O be set ; :: thesis: for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for g1 being Element of G
for h1 being Element of H1 st h1 = g1 holds
h1 " = g1 "
let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G
for g1 being Element of G
for h1 being Element of H1 st h1 = g1 holds
h1 " = g1 "
let H1 be StableSubgroup of G; :: thesis: for g1 being Element of G
for h1 being Element of H1 st h1 = g1 holds
h1 " = g1 "
let g1 be Element of G; :: thesis: for h1 being Element of H1 st h1 = g1 holds
h1 " = g1 "
let h1 be Element of H1; :: thesis: ( h1 = g1 implies h1 " = g1 " )
reconsider g9 = h1 " as Element of G by Th2;
A1: h1 * (h1 ") = 1_ H1 by GROUP_1:def 5;
assume h1 = g1 ; :: thesis: h1 " = g1 "
then g1 * g9 = 1_ H1 by A1, Th3
.= 1_ G by Th4 ;
hence h1 " = g1 " by GROUP_1:12; :: thesis: verum