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

A2: 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
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 f = I by A2, PARTFUN1:def 4;
A5: dom (proj (Carrier A,s),x) = product (Carrier A,s) by PRALG_3:def 2;
hence f . x = (proj (Carrier A,s),x) . f by PRALG_3:def 2
.= (proj (Carrier A,s),x) . g by A1, A3, A4
.= g . x by A5, PRALG_3:def 2 ;
:: thesis: verum

end;

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