now :: thesis: for S being set st S in rng <*G,F*> holds

S is AbGroup

hence
for bS is AbGroup

let S be set ; :: thesis: ( S in rng <*G,F*> implies S is AbGroup )

assume S in rng <*G,F*> ; :: thesis: S is AbGroup

then consider i being object such that

A1: ( i in dom <*G,F*> & <*G,F*> . i = S ) by FUNCT_1:def 3;

dom <*G,F*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;

then ( i = 1 or i = 2 ) by A1, TARSKI:def 2;

hence S is AbGroup by A1, FINSEQ_1:44; :: thesis: verum

end;assume S in rng <*G,F*> ; :: thesis: S is AbGroup

then consider i being object such that

A1: ( i in dom <*G,F*> & <*G,F*> . i = S ) by FUNCT_1:def 3;

dom <*G,F*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;

then ( i = 1 or i = 2 ) by A1, TARSKI:def 2;

hence S is AbGroup by A1, FINSEQ_1:44; :: thesis: verum

( not b