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 H1( 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 Function of NAT ,(bool the carrier of A) such that
A1:
B |^ n = F1 . n
and
A2:
( F1 . 0 = B & ( for n being Nat holds F1 . (n + 1) = H1(n,F1 . n) ) )
by Def8;
consider F2 being Function of NAT ,(bool the carrier of A) such that
A3:
B |^ (n + 1) = F2 . (n + 1)
and
A4:
( F2 . 0 = B & ( for n being Nat holds F2 . (n + 1) = H1(n,F2 . n) ) )
by Def8;
A5:
dom F1 = NAT
by FUNCT_2:def 1;
B5:
F1 . 0 = B
by A2;
C5:
for n being Nat holds F1 . (n + 1) = H1(n,F1 . n)
by A2;
A6:
dom F2 = NAT
by FUNCT_2:def 1;
B6:
F2 . 0 = B
by A4;
C6:
for n being Nat holds F2 . (n + 1) = H1(n,F2 . n)
by A4;
F1 = F2
from NAT_1:sch 15(A5, B5, C5, A6, B6, C6);
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, A2, A3; :: thesis: verum