consider p being FinSequence such that
A1: rng p = B by FINSEQ_1:73;
defpred S₁[ Nat] means ( $1 <= len p implies ex a being Nat ex A being bag of st
( a in dom p & a <= $1 & p . a = A & ( for c being Nat
for C being bag of st c in dom p & c <= $1 & p . c = C holds
C <= A,T ) ) );
p <> {} by A1;
then A2: 0 <> len p ;
A3: S₁[1]

proof

A4: 1 in dom p by A1, FINSEQ_3:34;
then p . 1 in B by A1, FUNCT_1:def 5;
then reconsider A = p . 1 as bag of by POLYNOM1:def 14;

now

let c be Nat; :: thesis: for C being bag of st c in dom p & c <= 1 & p . c = C holds
C <= A,T
let C be bag of ; :: thesis: ( c in dom p & c <= 1 & p . c = C implies C <= A,T )
assume A5: ( c in dom p & c <= 1 & p . c = C ) ; :: thesis: C <= A,T
1 <= c by A5, FINSEQ_3:27;
then C = A by A5, XXREAL_0:1;
hence C <= A,T by TERMORD:6; :: thesis: verum

end;

hence S₁[1] by A4; :: thesis: verum

end;

A6: for k being non empty Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non empty Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]

per cases ( k < len p or k >= len p ) ;

suppose A8: k < len p ; :: thesis: S₁[k + 1]

then consider a being Nat, A being bag of such that
A9: ( a in dom p & a <= k & p . a = A ) and
A10: for c being Nat
for C being bag of st c in dom p & c <= k & p . c = C holds
C <= A,T by A7;
A11: k + 1 <= len p by A8, NAT_1:13;
1 <= k + 1 by CHORD:1;
then A12: k + 1 in dom p by A11, FINSEQ_3:27;
then p . (k + 1) in B by A1, FUNCT_1:def 5;
then reconsider Ck = p . (k + 1) as bag of by POLYNOM1:def 14;
set m = max A,Ck,T;
A13: ( A <= max A,Ck,T,T & Ck <= max A,Ck,T,T ) by TERMORD:14;

per cases ( max A,Ck,T = A or max A,Ck,T = Ck ) by TERMORD:12;

suppose A14: max A,Ck,T = A ; :: thesis: S₁[k + 1]

A15: ( a in dom p & a <= k + 1 & p . a = A ) by A9, NAT_1:13;

now

let c be Nat; :: thesis: for C being bag of st c in dom p & c <= k + 1 & p . c = C holds
b₃ <= max A,Ck,T,T
let C be bag of ; :: thesis: ( c in dom p & c <= k + 1 & p . c = C implies b₂ <= max A,Ck,T,T )
assume A16: ( c in dom p & c <= k + 1 & p . c = C ) ; :: thesis: b₂ <= max A,Ck,T,T

per cases ( c = k + 1 or c < k + 1 ) by A16, XXREAL_0:1;

suppose c = k + 1 ; :: thesis: b₂ <= max A,Ck,T,T

hence C <= max A,Ck,T,T by A16, TERMORD:14; :: thesis: verum

end;

suppose c < k + 1 ; :: thesis: b₂ <= max A,Ck,T,T

then c <= k by NAT_1:13;
then C <= A,T by A10, A16;
hence C <= max A,Ck,T,T by A13, TERMORD:8; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] by A14, A15; :: thesis: verum

end;

suppose A17: max A,Ck,T = Ck ; :: thesis: S₁[k + 1]

now

let c be Nat; :: thesis: for C being bag of st c in dom p & c <= k + 1 & p . c = C holds
b₃ <= max A,Ck,T,T
let C be bag of ; :: thesis: ( c in dom p & c <= k + 1 & p . c = C implies b₂ <= max A,Ck,T,T )
assume A18: ( c in dom p & c <= k + 1 & p . c = C ) ; :: thesis: b₂ <= max A,Ck,T,T

per cases ( c = k + 1 or c < k + 1 ) by A18, XXREAL_0:1;

suppose c = k + 1 ; :: thesis: b₂ <= max A,Ck,T,T

hence C <= max A,Ck,T,T by A18, TERMORD:14; :: thesis: verum

end;

suppose c < k + 1 ; :: thesis: b₂ <= max A,Ck,T,T

then c <= k by NAT_1:13;
then C <= A,T by A10, A18;
hence C <= max A,Ck,T,T by A13, TERMORD:8; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] by A12, A17; :: thesis: verum

end;

end;

end;

suppose k >= len p ; :: thesis: S₁[k + 1]

hence S₁[k + 1] by NAT_1:13; :: thesis: verum

end;

end;

end;

for k being non empty Nat holds S₁[k] from NAT_1:sch 10(A3, A6);
then consider a being Nat, A being bag of such that
A19: ( a in dom p & a <= len p & p . a = A ) and
A20: for c being Nat
for C being bag of st c in dom p & c <= len p & p . c = C holds
C <= A,T by A2;
take A ; :: thesis: ( A in B & ( for x being bag of st x in B holds
x <= A,T ) )
thus A in B by A1, A19, FUNCT_1:def 5; :: thesis: for x being bag of st x in B holds
x <= A,T

now

let x be bag of ; :: thesis: ( x in B implies x <= A,T )
assume A21: x in B ; :: thesis: x <= A,T
consider y being Nat such that
A22: ( y in dom p & p . y = x ) by A1, A21, FINSEQ_2:11;
y <= len p by A22, FINSEQ_3:27;
hence x <= A,T by A20, A22; :: thesis: verum

end;

hence for x being bag of st x in B holds
x <= A,T ; :: thesis: verum