set A = the AbGroup;

take <* the AbGroup*> ; :: thesis: ( not <* the AbGroup*> is empty & <* the AbGroup*> is AbGroup-yielding )

thus not <* the AbGroup*> is empty ; :: thesis: <* the AbGroup*> is AbGroup-yielding

let x be set ; :: according to PRVECT_1:def 10 :: thesis: ( x in rng <* the AbGroup*> implies x is AbGroup )

assume that

A1: x in rng <* the AbGroup*> and

A2: x is not AbGroup ; :: thesis: contradiction

x in { the AbGroup} by A1, FINSEQ_1:38;

hence contradiction by A2, TARSKI:def 1; :: thesis: verum

take <* the AbGroup*> ; :: thesis: ( not <* the AbGroup*> is empty & <* the AbGroup*> is AbGroup-yielding )

thus not <* the AbGroup*> is empty ; :: thesis: <* the AbGroup*> is AbGroup-yielding

let x be set ; :: according to PRVECT_1:def 10 :: thesis: ( x in rng <* the AbGroup*> implies x is AbGroup )

assume that

A1: x in rng <* the AbGroup*> and

A2: x is not AbGroup ; :: thesis: contradiction

x in { the AbGroup} by A1, FINSEQ_1:38;

hence contradiction by A2, TARSKI:def 1; :: thesis: verum