let P, Q be FinSequence-membered set ; :: thesis: ( P c= Q implies for n being Nat holds P ^^ n c= Q ^^ n )
assume A1: P c= Q ; :: thesis: for n being Nat holds P ^^ n c= Q ^^ n
defpred S₁[ Nat] means P ^^ $1 c= Q ^^ $1;
P ^^ 0 = {{}} by Th6
.= Q ^^ 0 by Th6 ;
then A2: S₁[ 0 ] ;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
A5: P ^^ (n + 1) = (P ^^ n) ^ P by Th6;
Q ^^ (n + 1) = (Q ^^ n) ^ Q by Th6;
hence S₁[n + 1] by A1, A4, A5, Th16; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence for n being Nat holds P ^^ n c= Q ^^ n ; :: thesis: verum