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 CARD_3:def 17;
hence f . x = (proj ( the Sorts of A,x)) . f by CARD_3:def 17
.= (proj ( the Sorts of A,x)) . g by A1
.= g . x by A2, CARD_3:def 17 ;
:: thesis: verum

end;

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