let S be non empty ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for f, g being Element of product the Sorts of A st ( for i being set holds (proj the Sorts of A,i) . f = (proj the Sorts of A,i) . g ) holds
f = g
let A be non-empty MSAlgebra of S; :: thesis: for f, g being Element of product the Sorts of A st ( for i being set holds (proj the Sorts of A,i) . f = (proj the Sorts of A,i) . g ) holds
f = g
let f, g be Element of product the Sorts of A; :: thesis: ( ( for i being set holds (proj the Sorts of A,i) . f = (proj the Sorts of A,i) . g ) implies f = g )
assume A1: for i being set holds (proj the Sorts of A,i) . f = (proj the Sorts of A,i) . g ; :: thesis: f = g
set X = the Sorts of A;

now

thus dom f = dom the Sorts of A by CARD_3:18
.= dom g by CARD_3:18 ; :: thesis: for x being set st x in dom f holds
f . x = g . x
let x be set ; :: thesis: ( x in dom f implies f . x = g . x )
assume x in dom f ; :: thesis: f . x = g . x
A2: dom (proj the Sorts of A,x) = product the Sorts of A by PRALG_3:def 2;
hence f . x = (proj the Sorts of A,x) . f by PRALG_3:def 2
.= (proj the Sorts of A,x) . g by A1
.= g . x by A2, PRALG_3:def 2 ;
:: thesis: verum

end;

hence f = g by FUNCT_1:9; :: thesis: verum