let A be Universal_Algebra; :: thesis: for B being Subset of A
for n being Nat
for x being set holds
( x in B |^ (n + 1) iff ( x in B 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; :: thesis: for n being Nat
for x being set holds
( x in B |^ (n + 1) iff ( x in B 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 ) ) )
defpred S₁[ Nat] means for x being set holds
( not x in B |^ ($1 + 1) or x in B 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 |^ $1 ) );
A1: B |^ 0 = B by Th18;
then A2: S₁[ 0 ] by Th20;

A3: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

let x be set ; :: thesis: ( not x in B |^ ((n + 1) + 1) or x in B 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 + 1) ) )
assume x in B |^ ((n + 1) + 1) ; :: thesis: ( x in B 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 + 1) ) )
then A5: ( x in B |^ (n + 1) 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 + 1) ) ) by Th20;

now :: thesis: ( 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 ) implies 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 + 1) ) )

given o being Element of dom the charact of A, p being Element of the carrier of A * such that A6: x = (Den (o,A)) . p and
A7: p in dom (Den (o,A)) and
A8: rng p c= B |^ n ; :: thesis: 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 + 1) )
take o = o; :: thesis: 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 + 1) )
take p = p; :: thesis: ( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ (n + 1) )
n <= n + 1 by NAT_1:13;
then B |^ n c= B |^ (n + 1) by Th21;
hence ( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ (n + 1) ) by A6, A7, A8; :: thesis: verum

end;

hence ( x in B 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 + 1) ) ) by A4, A5; :: thesis: verum

end;

end;

A9: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
let n be Nat; :: thesis: for x being set holds
( x in B |^ (n + 1) iff ( x in B 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 x be set ; :: thesis: ( x in B |^ (n + 1) iff ( x in B 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 c= B |^ n by A1, Th21;
hence ( x in B |^ (n + 1) iff ( x in B 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 ) ) ) by A9, Th20; :: thesis: verum