let S be non empty ManySortedSign ; 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; 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; ( ( 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
; f = g
set X = the Sorts of A;
hence
f = g
; verum