let S be non empty ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for f, g being Element of product the Sorts of A st ( for i being object holds (proj ( the Sorts of A,i)) . f = (proj ( the Sorts of A,i)) . g ) holds
f = g
let A be non-empty MSAlgebra over S; :: thesis: for f, g being Element of product the Sorts of A st ( for i being object 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 object holds (proj ( the Sorts of A,i)) . f = (proj ( the Sorts of A,i)) . g ) implies f = g )
assume A1: for i being object 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 :: thesis: ( dom f = dom g & ( for x being object st x in dom f holds
f . x = g . x ) )

thus dom f = dom the Sorts of A by CARD_3:9
.= dom g by CARD_3:9 ; :: thesis: for x being object st x in dom f holds
f . x = g . x
let x be object ; :: 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 16;
hence f . x = (proj ( the Sorts of A,x)) . f by CARD_3:def 16
.= (proj ( the Sorts of A,x)) . g by A1
.= g . x by A2, CARD_3:def 16 ;
:: thesis: verum

end;

hence f = g ; :: thesis: verum