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

A2: now :: thesis: for x being set st S₁[x] holds
x in the carrier of (product F)

let x be set ; :: thesis: ( S₁[x] implies x in the carrier of (product F) )
assume A3: S₁[x] ; :: thesis: x in the carrier of (product F)
A4: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
ex Ri being 1-sorted st
( Ri = F . i & (Carrier F) . i = the carrier of Ri ) by PRALG_1:def 15;
hence x in the carrier of (product F) by A3, A4, YELLOW17:2; :: thesis: verum

end;

let x be set ; :: thesis: ( x in H iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) )
( x in H iff ( x in the carrier of (product F) & S₁[x] ) ) by A1;
hence ( x in H iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) by A2; :: thesis: verum