consider A being AbGroup;
take <*A*> ; :: thesis: ( not <*A*> is empty & <*A*> is AbGroup-yielding )
thus not <*A*> is empty ; :: thesis: <*A*> is AbGroup-yielding
let x be set ; :: according to PRVECT_1:def 11 :: thesis: ( x in rng <*A*> implies x is AbGroup )
assume that
A1: x in rng <*A*> and
A2: x is not AbGroup ; :: thesis: contradiction
x in {A} by A1, FINSEQ_1:55;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum