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:9;
hence dom f = dom g by CARD_3:9; :: thesis: for x being set st x in dom f holds
f . x = g . x
A2: dom f = I by PARTFUN1:def 2;
let x be set ; :: thesis: ( x in dom f implies f . x = g . x )
assume A3: x in dom f ; :: thesis: f . x = g . x
A4: 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, A3, A2
.= g . x by A4, CARD_3:def 16 ;
:: thesis: verum

end;

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