deffunc H₁( object ) -> set = x +* (i,$1);
A1: for r being object st r in X . i holds
H₁(r) in product X

proof

let r be object ; :: thesis: ( r in X . i implies H₁(r) in product X )
assume A2: r in X . i ; :: thesis: H₁(r) in product X

per cases ( not i in dom x or i in dom x ) ;

suppose not i in dom x ; :: thesis: H₁(r) in product X

then H₁(r) = x by FUNCT_7:def 3;
hence H₁(r) in product X ; :: thesis: verum

end;

suppose A4: i in dom x ; :: thesis: H₁(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 H₁(r) = dom X by A5, FUNCT_7:30;
for j being object st j in dom X holds
H₁(r) . j in X . j

proof

let j be object ; :: thesis: ( j in dom X implies H₁(r) . j in X . j )
assume A7: j in dom X ; :: thesis: H₁(r) . j in X . j

per cases ( j = i or j <> i ) ;

suppose j = i ; :: thesis: H₁(r) . j in X . j

hence H₁(r) . j in X . j by A2, A4, FUNCT_7:31; :: thesis: verum

end;

suppose j <> i ; :: thesis: H₁(r) . j in X . j

then H₁(r) . j = x . j by FUNCT_7:32;
hence H₁(r) . j in X . j by A5, A7; :: thesis: verum

end;

end;

end;

hence H₁(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 = H₁(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