let X be set ; :: thesis: for E being non empty set
for v, w being Element of E ^omega
for TS being non empty transition-system over (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 v, w being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds w -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ w) -succ_of (X,TS))}
let v, w be Element of E ^omega ; :: thesis: for TS being non empty transition-system over (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 over (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 ^ {}) -succ_of (X,TS))}
.= {((v ^ {}) -succ_of (X,TS))}
.= {((v ^ u) -succ_of (X,TS))} by A3 ;
:: thesis: verum

end;

A4: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

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

now :: thesis: for u being Element of E ^omega st len u <= k + 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))}

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:25;

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 :: thesis: for x being object st x in {((v ^ u) -succ_of (X,TS))} holds
x in u -succ_of ({(v -succ_of (X,TS))},(_bool TS))

let x be object ; :: 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 Th29;
then A11: v -succ_of (X,TS),u ==>* x, _bool TS by A8, Th13;
( 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 :: thesis: for x being object st x in u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) holds
x in {((v ^ u) -succ_of (X,TS))}

let x be object ; :: 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, Th13, TARSKI:def 1;
then P = (v ^ u) -succ_of (X,TS) by Th29;
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 over (Lex E) \/ {(<%> E)} by Th30;
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 Th29
.= 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:27 ;
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