let A be ECIW-strict preIfWhileAlgebra; :: thesis:
set B = ElementaryInstructions A;
let x be set ; :: thesis:
let n be Nat; :: thesis:
assume A1: x in (ElementaryInstructions A) |^ (n + 1) ; :: thesis:
then reconsider I = x as Element of A ;
assume A2: x nin (ElementaryInstructions A) |^ n ; :: thesis:
assume A3: x <> EmptyIns A ; :: thesis:
assume A4: for I1, I2 being Element of A holds
( not x = I1 \; I2 or not I1 in (ElementaryInstructions A) |^ n or not I2 in (ElementaryInstructions A) |^ n ) ; :: thesis:
assume A5: for C, I1, I2 being Element of A holds
( not x = if-then-else C,I1,I2 or not C in (ElementaryInstructions A) |^ n or not I1 in (ElementaryInstructions A) |^ n or not I2 in (ElementaryInstructions A) |^ n ) ; :: thesis:
(ElementaryInstructions A) |^ (n + 1) = ((ElementaryInstructions A) |^ n) \/ { ((Den o,A) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den o,A) & rng p c= (ElementaryInstructions A) |^ n ) } by Th19;
then x in { ((Den o,A) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den o,A) & rng p c= (ElementaryInstructions A) |^ n ) } by A1, A2, XBOOLE_0:def 3;
then consider o being Element of dom the charact of A, p being Element of the carrier of A * such that
A6: ( I = (Den o,A) . p & p in dom (Den o,A) & rng p c= (ElementaryInstructions A) |^ n ) ;
reconsider no = o as Element of NAT ;
reconsider oo = Den o,A as Element of Operations A ;
len (signature A) = len the charact of A by UNIALG_1:def 11;
then A7: dom (signature A) = dom the charact of A by FINSEQ_3:31;
A8: len p = arity oo by A6, UNIALG_1:def 10
.= (signature A) . no by A7, UNIALG_1:def 11
.= ECIW-signature . o by Def27 ;
A9: In o,(dom the charact of A) = o by FUNCT_7:def 1;
A10: ( 1 in Seg 2 & 2 in Seg 2 & 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) ;

per cases by Th55;

suppose S: o = 1 ; :: thesis:

then ECIW-signature . o = 0 by Th54;
then p = {} by A8;
then x = (Den o,A) . {} by A6;
then x = (Den (In 1,(dom the charact of A)),A) . {} by A9, S;
then x = EmptyIns A ;
hence ex C, I being Element of A st
( x = while C,I & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) by A3; :: thesis:

end;

suppose A11: o = 2 ; :: thesis:

then A12: ( p = <*(p . 1),(p . 2)*> & dom p = Seg 2 ) by A8, Th54, FINSEQ_1:61, FINSEQ_1:def 3;
then A13: ( p . 1 in rng p & p . 2 in rng p ) by A10, FUNCT_1:def 5;
then reconsider I1 = p . 1, I2 = p . 2 as Element of A ;
I = I1 \; I2 by A6, A11, A12, FUNCT_7:def 1;
hence ex C, I being Element of A st
( x = while C,I & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) by A4, A6, A13; :: thesis:

end;

suppose A14: o = 3 ; :: thesis:

then A15: ( p = <*(p . 1),(p . 2),(p . 3)*> & dom p = Seg 3 ) by A8, Th54, FINSEQ_1:62, FINSEQ_1:def 3;
then A16: ( p . 1 in rng p & p . 2 in rng p & p . 3 in rng p ) by A10, FUNCT_1:def 5;
then reconsider C = p . 1, I1 = p . 2, I2 = p . 3 as Element of A ;
I = if-then-else C,I1,I2 by A6, A14, A15, FUNCT_7:def 1;
hence ex C, I being Element of A st
( x = while C,I & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) by A5, A6, A16; :: thesis:

end;

suppose A17: o = 4 ; :: thesis:

then A18: ( p = <*(p . 1),(p . 2)*> & dom p = Seg 2 ) by A8, Th54, FINSEQ_1:61, FINSEQ_1:def 3;
then A19: ( p . 1 in rng p & p . 2 in rng p ) by A10, FUNCT_1:def 5;
then reconsider I1 = p . 1, I2 = p . 2 as Element of A ;
I = while I1,I2 by A6, A17, A18, FUNCT_7:def 1;
hence ex C, I being Element of A st
( x = while C,I & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) by A6, A19; :: thesis:

end;