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

now :: thesis: for x being object st x in dom f1 holds
f1 . x = f2 . x

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

end;

hence f1 = f2 by A41; :: thesis: verum