reconsider x1 = x as Element of product (carr G) by Th10;
defpred S1[ 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 S1[r,y]
proof
let r be Element of (G . i); :: thesis: ex y being Element of the carrier of (product G) st S1[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 S1[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 S1[r,f . r] from FUNCT_2:sch 3(A1);
 hence ex b1 being Function of (G . i),(product G) st
for r being Element of (G . i) holds b1 . r = x +* (i,r) ; :: thesis: verum