deffunc H1( object ) -> set = x +* (i,$1);
A1: for r being object st r in X . i holds
H1(r) in product X
proof
let r be object ; :: thesis: ( r in X . i implies H1(r) in product X )
assume A2: r in X . i ; :: thesis: H1(r) in product X
per cases ( not i in dom x or i in dom x ) ;
suppose A4: i in dom x ; :: thesis: H1(r) in product X
consider g being Function such that
A5: ( x = g & dom g = dom X & ( for j being object st j in dom X holds
g . j in X . j ) ) by CARD_3:def 5;
A6: dom H1(r) = dom X by A5, FUNCT_7:30;
for j being object st j in dom X holds
H1(r) . j in X . j
proof
let j be object ; :: thesis: ( j in dom X implies H1(r) . j in X . j )
assume A7: j in dom X ; :: thesis: H1(r) . j in X . j
per cases ( j = i or j <> i ) ;
suppose j = i ; :: thesis: H1(r) . j in X . j
hence H1(r) . j in X . j by A2, A4, FUNCT_7:31; :: thesis: verum
end;
suppose j <> i ; :: thesis: H1(r) . j in X . j
then H1(r) . j = x . j by FUNCT_7:32;
hence H1(r) . j in X . j by A5, A7; :: thesis: verum
end;
end;
end;
hence H1(r) in product X by A6, CARD_3:def 5; :: thesis: verum
end;
end;
end;
consider f being Function of (X . i),(product X) such that
A9: for r being object st r in X . i holds
f . r = H1(r) from FUNCT_2:sch 2(A1);
 take f ; :: thesis: for r being object st r in X . i holds
f . r = x +* (i,r)
thus for r being object st r in X . i holds
f . r = x +* (i,r) by A9; :: thesis: verum