let G be Group; :: thesis: for H being Subgroup of G

for h being Element of G st h in H holds

H * h c= the carrier of H

let H be Subgroup of G; :: thesis: for h being Element of G st h in H holds

H * h c= the carrier of H

let h be Element of G; :: thesis: ( h in H implies H * h c= the carrier of H )

assume A1: h in H ; :: thesis: H * h c= the carrier of H

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in H * h or a in the carrier of H )

assume a in H * h ; :: thesis: a in the carrier of H

then consider g being Element of G such that

A2: a = g * h and

A3: g in H by GROUP_2:104;

g * h in H by A1, A3, GROUP_2:50;

hence a in the carrier of H by A2; :: thesis: verum

for h being Element of G st h in H holds

H * h c= the carrier of H

let H be Subgroup of G; :: thesis: for h being Element of G st h in H holds

H * h c= the carrier of H

let h be Element of G; :: thesis: ( h in H implies H * h c= the carrier of H )

assume A1: h in H ; :: thesis: H * h c= the carrier of H

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in H * h or a in the carrier of H )

assume a in H * h ; :: thesis: a in the carrier of H

then consider g being Element of G such that

A2: a = g * h and

A3: g in H by GROUP_2:104;

g * h in H by A1, A3, GROUP_2:50;

hence a in the carrier of H by A2; :: thesis: verum