set CF = the carrier of (product F);

defpred S_{1}[ 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_{1}[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;

( x in H iff ( x in the carrier of (product F) & S_{1}[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

defpred S

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

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_{1}[x] holds

x in the carrier of (product F)

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 the carrier of (product F)

let x be set ; :: thesis: ( S_{1}[x] implies x in the carrier of (product F) )

assume A3: S_{1}[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;assume A3: S

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

( x in H iff ( x in the carrier of (product F) & S

hence ( x in H iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) by A2; :: thesis: verum