let A be Universal_Algebra; :: thesis: for B being Subset of A
for n being Nat holds 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 ) }
let B be Subset of A; :: thesis: for n being Nat holds 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 ) }
let n be Nat; :: thesis: 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 ) }
deffunc H₁( set , set ) -> set = $2 \/ { ((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= $2 ) } ;
consider F1 being sequence of (bool the carrier of A) such that
A1: B |^ n = F1 . n and
A2: F1 . 0 = B and
A3: for n being Nat holds F1 . (n + 1) = H₁(n,F1 . n) by Def8;
consider F2 being sequence of (bool the carrier of A) such that
A4: B |^ (n + 1) = F2 . (n + 1) and
A5: F2 . 0 = B and
A6: for n being Nat holds F2 . (n + 1) = H₁(n,F2 . n) by Def8;
A7: dom F1 = NAT by FUNCT_2:def 1;
A8: F1 . 0 = B by A2;
A9: for n being Nat holds F1 . (n + 1) = H₁(n,F1 . n) by A3;
A10: dom F2 = NAT by FUNCT_2:def 1;
A11: F2 . 0 = B by A5;
A12: for n being Nat holds F2 . (n + 1) = H₁(n,F2 . n) by A6;
F1 = F2 from NAT_1:sch 15(A7, A8, A9, A10, A11, A12);
hence 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 A1, A3, A4; :: thesis: verum