let A be preIfWhileAlgebra; :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: 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; :: thesis: verum