consider p being FinSequence such that

A1: rng p = B by FINSEQ_1:52;

defpred S_{1}[ 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 S_{1}[k] holds

S_{1}[k + 1]

A22: S_{1}[1]
_{1}[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

x <= A,T ; :: thesis: verum

A1: rng p = B by FINSEQ_1:52;

defpred S

( 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 S

S

proof

A21:
p <> {}
by A1;
let k be non zero Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: S_{1}[k]
; :: thesis: S_{1}[k + 1]

end;assume A3: S

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

end;

suppose A4:
k < len p
; :: thesis: S_{1}[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;

end;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;

end;

suppose A12:
max (A,Ck,T) = A
; :: thesis: S_{1}[k + 1]

hence S_{1}[k + 1]
by A7, A9, A12, A13; :: thesis: verum

end;

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

a <= k + 1
by A8, NAT_1:13;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

b_{3} <= max (A,Ck,T),T

let C be bag of n; :: thesis: ( c in dom p & c <= k + 1 & p . c = C implies b_{2} <= max (A,Ck,T),T )

assume that

A14: c in dom p and

A15: c <= k + 1 and

A16: p . c = C ; :: thesis: b_{2} <= max (A,Ck,T),T

end;b

let C be bag of n; :: thesis: ( c in dom p & c <= k + 1 & p . c = C implies b

assume that

A14: c in dom p and

A15: c <= k + 1 and

A16: p . c = C ; :: thesis: b

hence S

suppose A17:
max (A,Ck,T) = Ck
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
by A6, A17; :: thesis: verum

end;

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

hence
Sfor 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

b_{3} <= max (A,Ck,T),T

let C be bag of n; :: thesis: ( c in dom p & c <= k + 1 & p . c = C implies b_{2} <= max (A,Ck,T),T )

assume that

A18: c in dom p and

A19: c <= k + 1 and

A20: p . c = C ; :: thesis: b_{2} <= max (A,Ck,T),T

end;b

let C be bag of n; :: thesis: ( c in dom p & c <= k + 1 & p . c = C implies b

assume that

A18: c in dom p and

A19: c <= k + 1 and

A20: p . c = C ; :: thesis: b

A22: S

proof

for k being non zero Nat holds S
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 ;

_{1}[1]
by A23; :: thesis: verum

end;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

hence
Sfor 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;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

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

hence
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;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

x <= A,T ; :: thesis: verum