reconsider x1 = x as Element of product (carr G) by Th10;
defpred S₁[ Element of (G . i), Element of the carrier of (product G)] means $2 = x1 +* (i,$1);
A1: for r being Element of (G . i) ex y being Element of the carrier of (product G) st S₁[r,y]

proof

let r be Element of (G . i); :: thesis: ex y being Element of the carrier of (product G) st S₁[r,y]
x1 +* (i,r) is Element of the carrier of (product G) by Th11;
hence ex y being Element of the carrier of (product G) st S₁[r,y] ; :: thesis: verum

end;

ex f being Function of the carrier of (G . i), the carrier of (product G) st
for r being Element of (G . i) holds S₁[r,f . r] from FUNCT_2:sch 3(A1);
hence ex b₁ being Function of (G . i),(product G) st
for r being Element of (G . i) holds b₁ . r = x +* (i,r) ; :: thesis: verum