let X be set ; :: thesis: for E being non empty set
for w, v being Element of E ^omega
for TS being non empty transition-system of (Lex E) \/ {(<%> E)} holds w -succ_of {(v -succ_of X,TS)},(_bool TS) = {((v ^ w) -succ_of X,TS)}
let E be non empty set ; :: thesis: for w, v being Element of E ^omega
for TS being non empty transition-system of (Lex E) \/ {(<%> E)} holds w -succ_of {(v -succ_of X,TS)},(_bool TS) = {((v ^ w) -succ_of X,TS)}
let w, v be Element of E ^omega ; :: thesis: for TS being non empty transition-system of (Lex E) \/ {(<%> E)} holds w -succ_of {(v -succ_of X,TS)},(_bool TS) = {((v ^ w) -succ_of X,TS)}
let TS be non empty transition-system of (Lex E) \/ {(<%> E)}; :: thesis: w -succ_of {(v -succ_of X,TS)},(_bool TS) = {((v ^ w) -succ_of X,TS)}
defpred S₁[ Nat] means for u being Element of E ^omega st len u <= $1 holds
for v being Element of E ^omega holds u -succ_of {(v -succ_of X,TS)},(_bool TS) = {((v ^ u) -succ_of X,TS)};
A1: not <%> E in rng (dom the Tran of (_bool TS)) by Th8;
A2: S₁[ 0 ]

proof

let u be Element of E ^omega ; :: thesis: ( len u <= 0 implies for v being Element of E ^omega holds u -succ_of {(v -succ_of X,TS)},(_bool TS) = {((v ^ u) -succ_of X,TS)} )
assume len u <= 0 ; :: thesis: for v being Element of E ^omega holds u -succ_of {(v -succ_of X,TS)},(_bool TS) = {((v ^ u) -succ_of X,TS)}
then A3: u = <%> E ;
let v be Element of E ^omega ; :: thesis: u -succ_of {(v -succ_of X,TS)},(_bool TS) = {((v ^ u) -succ_of X,TS)}
reconsider vso = {(v -succ_of X,TS)} as Subset of (_bool TS) by Def1;
u -succ_of vso,(_bool TS) = vso by A1, A3, REWRITE3:104;
hence u -succ_of {(v -succ_of X,TS)},(_bool TS) = {((v ^ u) -succ_of X,TS)} by A3, AFINSQ_1:32; :: thesis: verum

end;

A4: now

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]

now

let u be Element of E ^omega ; :: thesis: ( len u <= k + 1 implies for v being Element of E ^omega holds b₂ -succ_of {(b₃ -succ_of X,TS)},(_bool TS) = {((b₃ ^ b₂) -succ_of X,TS)} )
assume A6: len u <= k + 1 ; :: thesis: for v being Element of E ^omega holds b₂ -succ_of {(b₃ -succ_of X,TS)},(_bool TS) = {((b₃ ^ b₂) -succ_of X,TS)}
let v be Element of E ^omega ; :: thesis: b₁ -succ_of {(b₂ -succ_of X,TS)},(_bool TS) = {((b₂ ^ b₁) -succ_of X,TS)}

per cases ( k = 0 or k <> 0 ) ;

suppose A7: k = 0 ; :: thesis: b₁ -succ_of {(b₂ -succ_of X,TS)},(_bool TS) = {((b₂ ^ b₁) -succ_of X,TS)}

per cases ( len u = 0 or len u = 1 ) by A6, A7, NAT_1:26;

suppose len u = 0 ; :: thesis: b₁ -succ_of {(b₂ -succ_of X,TS)},(_bool TS) = {((b₂ ^ b₁) -succ_of X,TS)}

hence u -succ_of {(v -succ_of X,TS)},(_bool TS) = {((v ^ u) -succ_of X,TS)} by A2; :: thesis: verum

end;

suppose A8: len u = 1 ; :: thesis: b₁ -succ_of {(b₂ -succ_of X,TS)},(_bool TS) = {((b₂ ^ b₁) -succ_of X,TS)}

A9: now

let x be set ; :: thesis: ( x in {((v ^ u) -succ_of X,TS)} implies x in u -succ_of {(v -succ_of X,TS)},(_bool TS) )
assume A10: x in {((v ^ u) -succ_of X,TS)} ; :: thesis: x in u -succ_of {(v -succ_of X,TS)},(_bool TS)
then reconsider P = x as Element of (_bool TS) by Def1;
x = (v ^ u) -succ_of X,TS by A10, TARSKI:def 1;
then x = u -succ_of (v -succ_of X,TS),TS by Th30;
then A11: v -succ_of X,TS,u ==>* x, _bool TS by A8, Th14;
( v -succ_of X,TS is Element of (_bool TS) & v -succ_of X,TS in {(v -succ_of X,TS)} ) by Def1, TARSKI:def 1;
then P in u -succ_of {(v -succ_of X,TS)},(_bool TS) by A11, REWRITE3:103;
hence x in u -succ_of {(v -succ_of X,TS)},(_bool TS) ; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in u -succ_of {(v -succ_of X,TS)},(_bool TS) implies x in {((v ^ u) -succ_of X,TS)} )
assume A12: x in u -succ_of {(v -succ_of X,TS)},(_bool TS) ; :: thesis: x in {((v ^ u) -succ_of X,TS)}
then reconsider P = x as Element of (_bool TS) ;
consider Q being Element of (_bool TS) such that
A13: ( Q in {(v -succ_of X,TS)} & Q,u ==>* P, _bool TS ) by A12, REWRITE3:103;
( Q = v -succ_of X,TS & P = u -succ_of Q,TS ) by A8, A13, Th14, TARSKI:def 1;
then P = (v ^ u) -succ_of X,TS by Th30;
hence x in {((v ^ u) -succ_of X,TS)} by TARSKI:def 1; :: thesis: verum

end;

hence u -succ_of {(v -succ_of X,TS)},(_bool TS) = {((v ^ u) -succ_of X,TS)} by A9, TARSKI:2; :: thesis: verum

end;

end;

end;

suppose A14: k <> 0 ; :: thesis: b₁ -succ_of {(b₂ -succ_of X,TS)},(_bool TS) = {((b₂ ^ b₁) -succ_of X,TS)}

reconsider bTS = _bool TS as non empty transition-system of (Lex E) \/ {(<%> E)} by Th31;
consider v1, v2 being Element of E ^omega such that
A15: len v1 <= k and
A16: len v2 <= k and
A17: u = v1 ^ v2 by A6, A14, Th5;
A18: v1 -succ_of {(v -succ_of X,TS)},(_bool TS) = {((v ^ v1) -succ_of X,TS)} by A5, A15;
A19: the Tran of bTS = the Tran of (_bool TS) ;
then (v1 ^ v2) -succ_of {(v -succ_of X,TS)},(_bool TS) = (v1 ^ v2) -succ_of {(v -succ_of X,TS)},bTS by REWRITE3:105
.= v2 -succ_of (v1 -succ_of {(v -succ_of X,TS)},bTS),bTS by Th30
.= v2 -succ_of (v1 -succ_of {(v -succ_of X,TS)},(_bool TS)),bTS by A19, REWRITE3:105
.= v2 -succ_of (v1 -succ_of {(v -succ_of X,TS)},(_bool TS)),(_bool TS) by A19, REWRITE3:105
.= {(((v ^ v1) ^ v2) -succ_of X,TS)} by A5, A16, A18
.= {((v ^ (v1 ^ v2)) -succ_of X,TS)} by AFINSQ_1:30 ;
hence u -succ_of {(v -succ_of X,TS)},(_bool TS) = {((v ^ u) -succ_of X,TS)} by A17; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A4);
then ( len w <= len w implies w -succ_of {(v -succ_of X,TS)},(_bool TS) = {((v ^ w) -succ_of X,TS)} ) ;
hence w -succ_of {(v -succ_of X,TS)},(_bool TS) = {((v ^ w) -succ_of X,TS)} ; :: thesis: verum