let G be Group; :: thesis:
let N be Subgroup of G; :: thesis:
assume A1: for x, y being Element of G st y in N holds
(x * y) * (x ") in N ; :: thesis:
for x being Element of G holds x * N c= N * x

let x be Element of G; :: thesis:
let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: z in x * N ; :: thesis:
then reconsider z = z as Element of G ;
consider z1 being Element of G such that
A3: ( z = x * z1 & z1 in N ) by A2, GROUP_2:103;
A4: (x * z1) * (x ") in N by A1, A3;
((x * z1) * (x ")) * x = z by A3, GROUP_3:1;
hence z in N * x by A4, GROUP_2:104; :: thesis:

end;