let x be object ; :: thesis: for G being addGroup
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 addGroup; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ) :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;

given g1, g2 being Element of G such that A3: ( x = g1 + g2 & g1 in A ) and
A4: g2 in H ; :: thesis: x in A + H
thus x in A + H by A3, A4; :: thesis: verum