set CF = the carrier of ();
defpred S1[ set ] means ex g being Element of (F . i) st \$1 = (1_ ()) +* (i,g);
consider H being Subset of the carrier of () such that
A1: for x being set holds
( x in H iff ( x in the carrier of () & S1[x] ) ) from take H ; :: thesis: for x being set holds
( x in H iff ex g being Element of (F . i) st x = (1_ ()) +* (i,g) )

set Gi = F . i;
A2: now :: thesis: for x being set st S1[x] holds
x in the carrier of ()
let x be set ; :: thesis: ( S1[x] implies x in the carrier of () )
assume A3: S1[x] ; :: thesis: x in the carrier of ()
A4: the carrier of () = product () by GROUP_7:def 2;
ex Ri being 1-sorted st
( Ri = F . i & () . i = the carrier of Ri ) by PRALG_1:def 13;
hence x in the carrier of () by ; :: thesis: verum
end;
let x be set ; :: thesis: ( x in H iff ex g being Element of (F . i) st x = (1_ ()) +* (i,g) )
( x in H iff ( x in the carrier of () & S1[x] ) ) by A1;
hence ( x in H iff ex g being Element of (F . i) st x = (1_ ()) +* (i,g) ) by A2; :: thesis: verum