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

dom f = dom (Carrier (A,s)) by CARD_3:18;
hence dom f = dom g by CARD_3:18; :: thesis: for x being set st x in dom f holds
f . x = g . x
A3: dom f = I by PARTFUN1:def 4;
let x be set ; :: thesis: ( x in dom f implies f . x = g . x )
assume A4: x in dom f ; :: thesis: f . x = g . x
A5: dom (proj ((Carrier (A,s)),x)) = product (Carrier (A,s)) by CARD_3:def 17;
hence f . x = (proj ((Carrier (A,s)),x)) . f by CARD_3:def 17
.= (proj ((Carrier (A,s)),x)) . g by A1, A4, A3
.= g . x by A5, CARD_3:def 17 ;
:: thesis: verum

end;

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