defpred S₁[ set ] means ex x being set ex g being Function ex y being set st
( $1 = [x,y] & x in dom f & g = f . x & y in dom g );
let f1, f2 be Function; :: thesis:
assume that
A38: for t being set holds
( t in dom f1 iff S₁[t] ) and
A39: for x being set
for g being Function st x in dom f1 & g = f . (x `1) holds
f1 . x = g . (x `2) and
A40: for t being set holds
( t in dom f2 iff S₁[t] ) and
A41: for x being set
for g being Function st x in dom f2 & g = f . (x `1) holds
f2 . x = g . (x `2) ; :: thesis:
A42: dom f1 = dom f2 from XBOOLE_0:sch 2(A38, A40);

let x be set ; :: thesis:
assume A43: x in dom f1 ; :: thesis:
then consider z being set , g being Function, y being set such that
A44: x = [z,y] and
z in dom f and
A45: g = f . z and
y in dom g by A38;
A46: ( z = x `1 & y = x `2 ) by A44, MCART_1:7;
then f1 . x = g . y by A39, A43, A45;
hence f1 . x = f2 . x by A41, A42, A43, A45, A46; :: thesis:

end;