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