let D be non empty set ; :: thesis: for n being Element of NAT
for a being set
for M being ManySortedSet of {a} st M = a .--> D holds
((M # ) * (*--> a)) . n = Funcs (Seg n),D
let n be Element of NAT ; :: thesis: for a being set
for M being ManySortedSet of {a} st M = a .--> D holds
((M # ) * (*--> a)) . n = Funcs (Seg n),D
let a be set ; :: thesis: for M being ManySortedSet of {a} st M = a .--> D holds
((M # ) * (*--> a)) . n = Funcs (Seg n),D
let M be ManySortedSet of {a}; :: thesis: ( M = a .--> D implies ((M # ) * (*--> a)) . n = Funcs (Seg n),D )
assume A1: M = a .--> D ; :: thesis: ((M # ) * (*--> a)) . n = Funcs (Seg n),D
a is Element of {a} by TARSKI:def 1;
then n |-> a is FinSequence of {a} by FINSEQ_2:77;
then A2: n |-> a in {a} * by FINSEQ_1:def 11;
dom (*--> a) = NAT by FUNCT_2:def 1;
hence ((M # ) * (*--> a)) . n = (M # ) . ((*--> a) . n) by FUNCT_1:23
.= (M # ) . (n |-> a) by Def20
.= product ((a .--> D) * (n |-> a)) by A1, A2, Def19
.= product (n |-> D) by Th152
.= Funcs (Seg n),D by CARD_3:20 ;
:: thesis: verum