let A be Universal_Algebra; for B being Subset of A
for n being Nat
for x being set holds
( x in B |^ (n + 1) iff ( x in B |^ n or ex o being Element of dom the charact of A ex p being Element of the carrier of A * st
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ n ) ) )
let B be Subset of A; for n being Nat
for x being set holds
( x in B |^ (n + 1) iff ( x in B |^ n or ex o being Element of dom the charact of A ex p being Element of the carrier of A * st
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ n ) ) )
let n be Nat; for x being set holds
( x in B |^ (n + 1) iff ( x in B |^ n or ex o being Element of dom the charact of A ex p being Element of the carrier of A * st
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ n ) ) )
set Z = { ((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 x be set ; ( x in B |^ (n + 1) iff ( x in B |^ n or ex o being Element of dom the charact of A ex p being Element of the carrier of A * st
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ n ) ) )
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;
then
( x in B |^ (n + 1) iff ( x in B |^ n or x 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 XBOOLE_0:def 3;
hence
( x in B |^ (n + 1) iff ( x in B |^ n or ex o being Element of dom the charact of A ex p being Element of the carrier of A * st
( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ n ) ) )
; verum