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;
( pe in {{} } & rng pe = {} & dom (Den (In 1,(dom the charact of A)),A) = {{} } & {} c= B |^ n ) by Th42, TARSKI:def 1, XBOOLE_1:2;
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 ) } ;
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 A2: 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 A3: 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 A4: 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) )
then ( <*I1,I2*> in 2 -tuples_on the carrier of A & rng <*I1,I2*> = {I1,I2} & dom (Den (In 2,(dom the charact of A)),A) = 2 -tuples_on the carrier of A & {I1,I2} c= B |^ n ) by A3, Th44, CATALG_1:10, FINSEQ_2:147, ZFMISC_1:38;
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 ) } ;
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) )
( <*C,I1,I2*> in 3 -tuples_on the carrier of A & rng <*C,I1,I2*> = {C,I1,I2} & dom (Den (In 3,(dom the charact of A)),A) = 3 -tuples_on the carrier of A & {C,I1,I2} c= B |^ n ) by A2, A3, A4, Th47, CATALG_1:12, FINSEQ_2:148, JORDAN16:2;
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 ) } ;
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)
( <*C,I1*> in 2 -tuples_on the carrier of A & rng <*C,I1*> = {C,I1} & dom (Den (In 4,(dom the charact of A)),A) = 2 -tuples_on the carrier of A & {C,I1} c= B |^ n ) by A2, A3, Th48, CATALG_1:10, FINSEQ_2:147, ZFMISC_1:38;
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 ) } ;
hence while C,I1 in B |^ (n + 1) by A1, XBOOLE_0:def 3; :: thesis: verum