let x be object ; for G being Group
for A being Subset of G
for H being Subgroup of G holds
( x in A * H iff ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in H ) )
let G be Group; for A being Subset of G
for H being Subgroup of G holds
( x in A * H iff ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in H ) )
let A be Subset of G; for H being Subgroup of G holds
( x in A * H iff ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in H ) )
let H be Subgroup of G; ( x in A * H iff ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in H ) )
thus
( x in A * H implies ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in H ) )
( ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in H ) implies x in A * H )proof
assume
x in A * H
;
ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in H )
then consider g1,
g2 being
Element of
G such that A1:
(
x = g1 * g2 &
g1 in A )
and A2:
g2 in carr H
;
g2 in H
by A2;
hence
ex
g1,
g2 being
Element of
G st
(
x = g1 * g2 &
g1 in A &
g2 in H )
by A1;
verum
end;
given g1, g2 being Element of G such that A3:
( x = g1 * g2 & g1 in A )
and
A4:
g2 in H
; x in A * H
g2 in carr H
by A4;
hence
x in A * H
by A3; verum