let X be non empty disjoint_with_NAT set ; :: thesis: for S being non empty FinSequence of NAT
for i being Nat st i in dom S holds
for p being FinSequence of (FreeUnivAlgNSG S,X) st len p = S . i holds
(Den (In i,(dom the charact of (FreeUnivAlgNSG S,X))),(FreeUnivAlgNSG S,X)) . p = i -tree p
let S be non empty FinSequence of NAT ; :: thesis: for i being Nat st i in dom S holds
for p being FinSequence of (FreeUnivAlgNSG S,X) st len p = S . i holds
(Den (In i,(dom the charact of (FreeUnivAlgNSG S,X))),(FreeUnivAlgNSG S,X)) . p = i -tree p
reconsider S' = S as non empty FinSequence of omega ;
set G = DTConUA S,X;
set A = FreeUnivAlgNSG S,X;
let i be Nat; :: thesis: ( i in dom S implies for p being FinSequence of (FreeUnivAlgNSG S,X) st len p = S . i holds
(Den (In i,(dom the charact of (FreeUnivAlgNSG S,X))),(FreeUnivAlgNSG S,X)) . p = i -tree p )
assume A1: i in dom S ; :: thesis: for p being FinSequence of (FreeUnivAlgNSG S,X) st len p = S . i holds
(Den (In i,(dom the charact of (FreeUnivAlgNSG S,X))),(FreeUnivAlgNSG S,X)) . p = i -tree p
then A2: S' /. i = S . i by PARTFUN1:def 8;
let p be FinSequence of (FreeUnivAlgNSG S,X); :: thesis: ( len p = S . i implies (Den (In i,(dom the charact of (FreeUnivAlgNSG S,X))),(FreeUnivAlgNSG S,X)) . p = i -tree p )
assume len p = S . i ; :: thesis: (Den (In i,(dom the charact of (FreeUnivAlgNSG S,X))),(FreeUnivAlgNSG S,X)) . p = i -tree p
then p is Element of (S' /. i) -tuples_on (TS (DTConUA S,X)) by A2, FINSEQ_2:110;
then p in (S' /. i) -tuples_on (TS (DTConUA S,X)) ;
then A3: p in dom (FreeOpNSG i,S,X) by A1, FREEALG:def 11;
len the charact of (FreeUnivAlgNSG S,X) = len S by FREEALG:def 12;
then dom the charact of (FreeUnivAlgNSG S,X) = dom S by FINSEQ_3:31;
then In i,(dom the charact of (FreeUnivAlgNSG S,X)) = i by A1, FUNCT_7:def 1;
hence (Den (In i,(dom the charact of (FreeUnivAlgNSG S,X))),(FreeUnivAlgNSG S,X)) . p = (FreeOpNSG i,S,X) . p by A1, FREEALG:def 12
.= (Sym i,S,X) -tree p by A1, A3, FREEALG:def 11
.= i -tree p by A1, FREEALG:def 10 ;
:: thesis: verum