let g1, g2 be ManySortedFunction of dom f; :: thesis: ( ( for x being object st x in dom f holds
g1 . x = proj (f,x) ) & ( for x being object st x in dom f holds
g2 . x = proj (f,x) ) implies g1 = g2 )
assume that
A2: for x being object st x in dom f holds
g1 . x = proj (f,x) and
A3: for x being object st x in dom f holds
g2 . x = proj (f,x) ; :: thesis: g1 = g2

now :: thesis: for x being object st x in dom f holds
g1 . x = g2 . x

let x be object ; :: thesis: ( x in dom f implies g1 . x = g2 . x )
assume A4: x in dom f ; :: thesis: g1 . x = g2 . x
hence g1 . x = proj (f,x) by A2
.= g2 . x by A3, A4 ;
:: thesis: verum

end;

hence g1 = g2 by PBOOLE:3; :: thesis: verum