let S be non empty non void ManySortedSign ; :: thesis: for I being non empty set
for s being Element of S
for A being MSAlgebra-Family of I,S
for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds
f = g
let I be non empty set ; :: thesis: for s being Element of S
for A being MSAlgebra-Family of I,S
for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds
f = g
let s be Element of S; :: thesis: for A being MSAlgebra-Family of I,S
for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds
f = g
let A be MSAlgebra-Family of I,S; :: thesis: for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds
f = g
let f, g be Element of product (Carrier (A,s)); :: thesis: ( ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) implies f = g )
assume A1: for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ; :: thesis: f = g

now :: thesis: ( dom f = dom g & ( for x being object st x in dom f holds
f . x = g . x ) )

dom f = dom (Carrier (A,s)) by CARD_3:9;
hence dom f = 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 A2: x in dom f ; :: thesis: f . x = g . x
A3: dom (proj ((Carrier (A,s)),x)) = product (Carrier (A,s)) by CARD_3:def 16;
hence f . x = (proj ((Carrier (A,s)),x)) . f by CARD_3:def 16
.= (proj ((Carrier (A,s)),x)) . g by A1, A2
.= g . x by A3, CARD_3:def 16 ;
:: thesis: verum

end;

hence f = g ; :: thesis: verum