consider p being FinSequence such that
A1: rng p = B by FINSEQ_1:52;
defpred S1[ Nat] means ( $1 <= len p implies ex a being Nat ex A being bag of n st
( a in dom p & a <= $1 & p . a = A & ( for c being Nat
for C being bag of n st c in dom p & c <= $1 & p . c = C holds
C <= A,T ) ) );
A2: for k being non zero Nat st S1[k] holds
S1[k + 1]
proof
let k be non zero Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[k + 1]
per cases ( k < len p or k >= len p ) ;
suppose A4: k < len p ; :: thesis: S1[k + 1]
A5: 1 <= k + 1 by CHORD:1;
k + 1 <= len p by A4, NAT_1:13;
then A6: k + 1 in dom p by A5, FINSEQ_3:25;
then p . (k + 1) in B by A1, FUNCT_1:def 3;
then reconsider Ck = p . (k + 1) as bag of n ;
consider a being Nat, A being bag of n such that
A7: a in dom p and
A8: a <= k and
A9: p . a = A and
A10: for c being Nat
for C being bag of n st c in dom p & c <= k & p . c = C holds
C <= A,T by A3, A4;
set m = max (A,Ck,T);
A11: A <= 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 A12: max (A,Ck,T) = A ; :: thesis: S1[k + 1]
A13: now :: thesis: for c being Nat
for C being bag of n st c in dom p & c <= k + 1 & p . c = C holds
C <= max (A,Ck,T),T
let c be Nat; :: thesis: for C being bag of n st c in dom p & c <= k + 1 & p . c = C holds
b3 <= max (A,Ck,T),T
let C be bag of n; :: thesis: ( c in dom p & c <= k + 1 & p . c = C implies b2 <= max (A,Ck,T),T )
assume that
A14: c in dom p and
A15: c <= k + 1 and
A16: p . c = C ; :: thesis: b2 <= max (A,Ck,T),T
per cases ( c = k + 1 or c < k + 1 ) by A15, XXREAL_0:1;
suppose c = k + 1 ; :: thesis: b2 <= max (A,Ck,T),T
hence C <= max (A,Ck,T),T by A16, TERMORD:14; :: thesis: verum
end;
suppose c < k + 1 ; :: thesis: b2 <= max (A,Ck,T),T
then c <= k by NAT_1:13;
then C <= A,T by A10, A14, A16;
hence C <= max (A,Ck,T),T by A11, TERMORD:8; :: thesis: verum
end;
end;
end;
a <= k + 1 by A8, NAT_1:13;
hence S1[k + 1] by A7, A9, A12, A13; :: thesis: verum
end;
suppose A17: max (A,Ck,T) = Ck ; :: thesis: S1[k + 1]
now :: thesis: for c being Nat
for C being bag of n st c in dom p & c <= k + 1 & p . c = C holds
C <= max (A,Ck,T),T
let c be Nat; :: thesis: for C being bag of n st c in dom p & c <= k + 1 & p . c = C holds
b3 <= max (A,Ck,T),T
let C be bag of n; :: thesis: ( c in dom p & c <= k + 1 & p . c = C implies b2 <= max (A,Ck,T),T )
assume that
A18: c in dom p and
A19: c <= k + 1 and
A20: p . c = C ; :: thesis: b2 <= max (A,Ck,T),T
per cases ( c = k + 1 or c < k + 1 ) by A19, XXREAL_0:1;
suppose c = k + 1 ; :: thesis: b2 <= max (A,Ck,T),T
hence C <= max (A,Ck,T),T by A20, TERMORD:14; :: thesis: verum
end;
suppose c < k + 1 ; :: thesis: b2 <= max (A,Ck,T),T
then c <= k by NAT_1:13;
then C <= A,T by A10, A18, A20;
hence C <= max (A,Ck,T),T by A11, TERMORD:8; :: thesis: verum
end;
end;
end;
hence S1[k + 1] by A6, A17; :: thesis: verum
end;
end;
end;
suppose k >= len p ; :: thesis: S1[k + 1]
hence S1[k + 1] by NAT_1:13; :: thesis: verum
end;
end;
end;
A21: p <> {} by A1;
A22: S1[1]
proof
A23: 1 in dom p by A1, FINSEQ_3:32;
then p . 1 in B by A1, FUNCT_1:def 3;
then reconsider A = p . 1 as bag of n ;
now :: thesis: for c being Nat
for C being bag of n st c in dom p & c <= 1 & p . c = C holds
C <= A,T
let c be Nat; :: thesis: for C being bag of n st c in dom p & c <= 1 & p . c = C holds
C <= A,T
let C be bag of n; :: thesis: ( c in dom p & c <= 1 & p . c = C implies C <= A,T )
assume that
A24: c in dom p and
A25: c <= 1 and
A26: p . c = C ; :: thesis: C <= A,T
1 <= c by A24, FINSEQ_3:25;
then C = A by A25, A26, XXREAL_0:1;
hence C <= A,T by TERMORD:6; :: thesis: verum
end;
hence S1[1] by A23; :: thesis: verum
end;
for k being non zero Nat holds S1[k] from NAT_1:sch 10(A22, A2);
 then consider a being Nat, A being bag of n such that
A27: a in dom p and
a <= len p and
A28: p . a = A and
A29: for c being Nat
for C being bag of n st c in dom p & c <= len p & p . c = C holds
C <= A,T by A21;
take A ; :: thesis: ( A in B & ( for x being bag of n st x in B holds
x <= A,T ) )
thus A in B by A1, A27, A28, FUNCT_1:def 3; :: thesis: for x being bag of n st x in B holds
x <= A,T
now :: thesis: for x being bag of n st x in B holds
x <= A,T
let x be bag of n; :: thesis: ( x in B implies x <= A,T )
assume x in B ; :: thesis: x <= A,T
then consider y being Nat such that
A30: y in dom p and
A31: p . y = x by A1, FINSEQ_2:10;
y <= len p by A30, FINSEQ_3:25;
hence x <= A,T by A29, A30, A31; :: thesis: verum
end;
hence for x being bag of n st x in B holds
x <= A,T ; :: thesis: verum