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 Th77;
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:13
.= (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:11 ;
:: thesis: verum