let P be non empty FinSequence-membered set ; :: thesis: for m, n being Nat holds (P ^^ n) |` m c= (P |` m) ^^ n
let m be Nat; :: thesis: for n being Nat holds (P ^^ n) |` m c= (P |` m) ^^ n
defpred S₁[ Nat] means (P ^^ $1) |` m c= (P |` m) ^^ $1;
P ^^ 0 = {{}} by POLNOT_1:6
.= (P |` m) ^^ 0 by POLNOT_1:6 ;
then A10: S₁[ 0 ] ;
A20: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A21: S₁[n] ; :: thesis: S₁[n + 1]
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (P ^^ (n + 1)) |` m or a in (P |` m) ^^ (n + 1) )
assume A22: a in (P ^^ (n + 1)) |` m ; :: thesis: a in (P |` m) ^^ (n + 1)
then reconsider p = a as FinSequence ;
p in P ^^ (n + 1) by A22;
then p in (P ^^ n) ^ P by POLNOT_1:6;
then consider q, r being FinSequence such that
A24: p = q ^ r and
A25: q in P ^^ n and
A26: r in P by POLNOT_1:def 2;
A30: len p <= m by A22, Lm19;
len p = (len q) + (len r) by A24, FINSEQ_1:22;
then ( len q <= len p & len r <= len p ) by NAT_1:11;
then ( len q <= m & len r <= m ) by A30, XXREAL_0:2;
then ( q in (P ^^ n) |` m & r in P |` m ) by A25, A26;
then p in ((P |` m) ^^ n) ^ (P |` m) by A21, A24, POLNOT_1:def 2;
hence a in (P |` m) ^^ (n + 1) by POLNOT_1:6; :: thesis: verum

end;

thus for n being Nat holds S₁[n] from NAT_1:sch 2(A10, A20); :: thesis: verum