let D be non empty set ; :: thesis: for n being 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 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 Th61;
then A2: n |-> a in {a} * by FINSEQ_1:def 11;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
dom (*--> a) = NAT by FUNCT_2:def 1;
hence ((M #) * (*--> a)) . n = (M #) . ((*--> a) . nn) by FUNCT_1:13
.= (M #) . (nn |-> a) by Def6
.= product ((a .--> D) * (n |-> a)) by A1, A2, Def5
.= product (n |-> D) by Th142
.= Funcs ((Seg n),D) by CARD_3:11 ;
:: thesis: verum