let A, B be Function; :: thesis: ( ( not S is empty & ( for x being set holds
( x in dom A iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom A holds
A . i = pi (S,i) ) & ( for x being set holds
( x in dom B iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom B holds
B . i = pi (S,i) ) implies A = B ) & ( S is empty & A = {} & B = {} implies A = B ) )
thus ( not S is empty & ( for x being set holds
( x in dom A iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom A holds
A . i = pi (S,i) ) & ( for x being set holds
( x in dom B iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom B holds
B . i = pi (S,i) ) implies A = B ) :: thesis: ( S is empty & A = {} & B = {} implies A = B )

proof

defpred S₂[ set ] means for f being Function st f in S holds
$1 in dom f;
assume that
not S is empty and
A7: for x being set holds
( x in dom A iff S₂[x] ) and
A8: for i being set st i in dom A holds
A . i = pi (S,i) and
A9: for x being set holds
( x in dom B iff S₂[x] ) and
A10: for i being set st i in dom B holds
B . i = pi (S,i) ; :: thesis: A = B
A11: dom A = dom B from XBOOLE_0:sch 2(A7, A9);

now

let i be set ; :: thesis: ( i in dom A implies A . i = B . i )
assume A12: i in dom A ; :: thesis: A . i = B . i
hence A . i = pi (S,i) by A8
.= B . i by A10, A11, A12 ;
:: thesis: verum

end;

hence A = B by A11, FUNCT_1:2; :: thesis: verum

end;

thus ( S is empty & A = {} & B = {} implies A = B ) ; :: thesis: verum