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 S9 = 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: S9 /. i = S . i by PARTFUN1:def 6;
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 (S9 /. i) -tuples_on (TS (DTConUA (S,X))) by A2, FINSEQ_2:92;
then p in (S9 /. i) -tuples_on (TS (DTConUA (S,X))) ;
then A3: p in dom (FreeOpNSG (i,S,X)) by A1, FREEALG:def 10;
len the charact of (FreeUnivAlgNSG (S,X)) = len S by FREEALG:def 11;
then dom the charact of (FreeUnivAlgNSG (S,X)) = dom S by FINSEQ_3:29;
then In (i,(dom the charact of (FreeUnivAlgNSG (S,X)))) = i by A1, SUBSET_1:def 8;
hence (Den ((In (i,(dom the charact of (FreeUnivAlgNSG (S,X))))),(FreeUnivAlgNSG (S,X)))) . p = (FreeOpNSG (i,S,X)) . p by FREEALG:def 11
.= (Sym (i,S,X)) -tree p by A1, A3, FREEALG:def 10
.= i -tree p by A1, FREEALG:def 9 ;
:: thesis: verum