let f, g be Function; :: thesis: ( dom f = DOM S & ( for i being set st i in dom f holds
f . i = pi (S,i) ) & dom g = DOM S & ( for i being set st i in dom g holds
g . i = pi (S,i) ) implies f = g )
assume that
Z1: dom f = DOM S and
Z2: for i being set st i in dom f holds
f . i = pi (S,i) and
Z3: dom g = DOM S and
Z4: for i being set st i in dom g holds
g . i = pi (S,i) ; :: thesis: f = g
for x being set st x in dom f holds
f . x = g . x

proof

let x be set ; :: thesis: ( x in dom f implies f . x = g . x )
assume Z: x in dom f ; :: thesis: f . x = g . x
hence f . x = pi (S,x) by Z2
.= g . x by Z1, Z3, Z, Z4 ;
:: thesis: verum

end;

hence f = g by Z1, Z3, FUNCT_1:def 11; :: thesis: verum