let A be preIfWhileAlgebra; for B being Subset of A
for n being Nat holds
( EmptyIns A in B |^ (n + 1) & ( for C, I1, I2 being Element of A st C in B |^ n & I1 in B |^ n & I2 in B |^ n holds
( I1 \; I2 in B |^ (n + 1) & if-then-else (C,I1,I2) in B |^ (n + 1) & while (C,I1) in B |^ (n + 1) ) ) )
let B be Subset of A; for n being Nat holds
( EmptyIns A in B |^ (n + 1) & ( for C, I1, I2 being Element of A st C in B |^ n & I1 in B |^ n & I2 in B |^ n holds
( I1 \; I2 in B |^ (n + 1) & if-then-else (C,I1,I2) in B |^ (n + 1) & while (C,I1) in B |^ (n + 1) ) ) )
let n be Nat; ( EmptyIns A in B |^ (n + 1) & ( for C, I1, I2 being Element of A st C in B |^ n & I1 in B |^ n & I2 in B |^ n holds
( I1 \; I2 in B |^ (n + 1) & if-then-else (C,I1,I2) in B |^ (n + 1) & while (C,I1) in B |^ (n + 1) ) ) )
set X = { ((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= B |^ n ) } ;
A1:
B |^ (n + 1) = (B |^ 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= B |^ n ) }
by Th19;
reconsider pe = <*> the carrier of A as Element of the carrier of A * by FINSEQ_1:def 11;
A2:
pe in {{}}
by TARSKI:def 1;
A3:
rng pe = {}
;
A4:
dom (Den ((In (1,(dom the charact of A))),A)) = {{}}
by Th42;
{} c= B |^ n
;
then
EmptyIns A 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= B |^ n ) }
by A2, A3, A4;
hence
EmptyIns A in B |^ (n + 1)
by A1, XBOOLE_0:def 3; for C, I1, I2 being Element of A st C in B |^ n & I1 in B |^ n & I2 in B |^ n holds
( I1 \; I2 in B |^ (n + 1) & if-then-else (C,I1,I2) in B |^ (n + 1) & while (C,I1) in B |^ (n + 1) )
let C, I1, I2 be Element of A; ( C in B |^ n & I1 in B |^ n & I2 in B |^ n implies ( I1 \; I2 in B |^ (n + 1) & if-then-else (C,I1,I2) in B |^ (n + 1) & while (C,I1) in B |^ (n + 1) ) )
assume A5:
C in B |^ n
; ( not I1 in B |^ n or not I2 in B |^ n or ( I1 \; I2 in B |^ (n + 1) & if-then-else (C,I1,I2) in B |^ (n + 1) & while (C,I1) in B |^ (n + 1) ) )
assume A6:
I1 in B |^ n
; ( not I2 in B |^ n or ( I1 \; I2 in B |^ (n + 1) & if-then-else (C,I1,I2) in B |^ (n + 1) & while (C,I1) in B |^ (n + 1) ) )
assume A7:
I2 in B |^ n
; ( I1 \; I2 in B |^ (n + 1) & if-then-else (C,I1,I2) in B |^ (n + 1) & while (C,I1) in B |^ (n + 1) )
A8:
<*I1,I2*> in 2 -tuples_on the carrier of A
by FINSEQ_2:137;
A9:
rng <*I1,I2*> = {I1,I2}
by FINSEQ_2:127;
A10:
dom (Den ((In (2,(dom the charact of A))),A)) = 2 -tuples_on the carrier of A
by Th44;
{I1,I2} c= B |^ n
by A6, A7, ZFMISC_1:32;
then
I1 \; I2 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= B |^ n ) }
by A8, A9, A10;
hence
I1 \; I2 in B |^ (n + 1)
by A1, XBOOLE_0:def 3; ( if-then-else (C,I1,I2) in B |^ (n + 1) & while (C,I1) in B |^ (n + 1) )
A11:
<*C,I1,I2*> in 3 -tuples_on the carrier of A
by FINSEQ_2:139;
A12:
rng <*C,I1,I2*> = {C,I1,I2}
by FINSEQ_2:128;
A13:
dom (Den ((In (3,(dom the charact of A))),A)) = 3 -tuples_on the carrier of A
by Th47;
{C,I1,I2} c= B |^ n
by A5, A6, A7, ZFMISC_1:133;
then
if-then-else (C,I1,I2) 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= B |^ n ) }
by A11, A12, A13;
hence
if-then-else (C,I1,I2) in B |^ (n + 1)
by A1, XBOOLE_0:def 3; while (C,I1) in B |^ (n + 1)
A14:
<*C,I1*> in 2 -tuples_on the carrier of A
by FINSEQ_2:137;
A15:
rng <*C,I1*> = {C,I1}
by FINSEQ_2:127;
A16:
dom (Den ((In (4,(dom the charact of A))),A)) = 2 -tuples_on the carrier of A
by Th48;
{C,I1} c= B |^ n
by A5, A6, ZFMISC_1:32;
then
while (C,I1) 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= B |^ n ) }
by A14, A15, A16;
hence
while (C,I1) in B |^ (n + 1)
by A1, XBOOLE_0:def 3; verum