let p be XFinSequence of NAT ; :: thesis: for n being Nat st rng p c= {0,n} holds
ex q being XFinSequence of NAT st
( len p = len q & rng q c= {0,n} & ( for k being Nat st k <= len p holds
(Sum (p | k)) + (Sum (q | k)) = n * k ) & ( for k being Nat st k in len p holds
q . k = n - (p . k) ) )
let n be Nat; :: thesis: ( rng p c= {0,n} implies ex q being XFinSequence of NAT st
( len p = len q & rng q c= {0,n} & ( for k being Nat st k <= len p holds
(Sum (p | k)) + (Sum (q | k)) = n * k ) & ( for k being Nat st k in len p holds
q . k = n - (p . k) ) ) )
assume A1: rng p c= {0,n} ; :: thesis: ex q being XFinSequence of NAT st
( len p = len q & rng q c= {0,n} & ( for k being Nat st k <= len p holds
(Sum (p | k)) + (Sum (q | k)) = n * k ) & ( for k being Nat st k in len p holds
q . k = n - (p . k) ) )
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
defpred S1[ set , set ] means for k being Nat st k = $1 holds
$2 = n - (p . k);
A2: for k being Nat st k in Segm (len p) holds
ex x being Element of {0,n} st S1[k,x]
proof
let k be Nat; :: thesis: ( k in Segm (len p) implies ex x being Element of {0,n} st S1[k,x] )
assume k in Segm (len p) ; :: thesis: ex x being Element of {0,n} st S1[k,x]
then p . k in rng p by FUNCT_1:3;
then ( p . k = 0 or p . k = n ) by A1, TARSKI:def 2;
then A3: n - (p . k) in {0,n} by TARSKI:def 2;
S1[k,n - (p . k)] ;
hence ex x being Element of {0,n} st S1[k,x] by A3; :: thesis: verum
end;
consider q being XFinSequence of {0,n} such that
A4: ( dom q = Segm (len p) & ( for k being Nat st k in Segm (len p) holds
S1[k,q . k] ) ) from STIRL2_1:sch 5(A2);
 reconsider q = q as XFinSequence of NAT ;
defpred S2[ Nat] means ( $1 <= len p implies (Sum (p | $1)) + (Sum (q | $1)) = n * $1 );
A5: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A6: S2[k] ; :: thesis: S2[k + 1]
set k1 = k + 1;
A7: k < k + 1 by NAT_1:13;
then A8: Segm k c= Segm (k + 1) by NAT_1:39;
then A9: (p | (k + 1)) | k = p | k by RELAT_1:74;
A10: (q | (k + 1)) | k = q | k by A8, RELAT_1:74;
assume A11: k + 1 <= len p ; :: thesis: (Sum (p | (k + 1))) + (Sum (q | (k + 1))) = n * (k + 1)
then A12: Segm (k + 1) c= Segm (len p) by NAT_1:39;
then A13: len (q | (k + 1)) = k + 1 by A4, RELAT_1:62;
then A14: q | (k + 1) = ((q | (k + 1)) | k) ^ <%((q | (k + 1)) . k)%> by AFINSQ_1:56;
len (p | (k + 1)) = k + 1 by A12, RELAT_1:62;
then A15: k in dom (p | (k + 1)) by A7, AFINSQ_1:86;
then A16: (p | (k + 1)) . k = p . k by FUNCT_1:47;
len (p | (k + 1)) = k + 1 by A12, RELAT_1:62;
then p | (k + 1) = ((p | (k + 1)) | k) ^ <%((p | (k + 1)) . k)%> by AFINSQ_1:56;
then Sum (p | (k + 1)) = (Sum (p | k)) + (Sum <%(p . k)%>) by A16, A9, AFINSQ_2:55;
then A17: Sum (p | (k + 1)) = (Sum (p | k)) + (p . k) by AFINSQ_2:53;
k < len p by A11, NAT_1:13;
then k in len p by AFINSQ_1:86;
then A18: q . k = n - (p . k) by A4;
(q | (k + 1)) . k = q . k by A13, A15, FUNCT_1:47;
then Sum (q | (k + 1)) = (Sum (q | k)) + (Sum <%(q . k)%>) by A14, A10, AFINSQ_2:55;
then Sum (q | (k + 1)) = (Sum (q | k)) + (n - (p . k)) by A18, AFINSQ_2:53;
hence (Sum (p | (k + 1))) + (Sum (q | (k + 1))) = n * (k + 1) by A6, A11, A17, NAT_1:13; :: thesis: verum
end;
take q ; :: thesis: ( len p = len q & rng q c= {0,n} & ( for k being Nat st k <= len p holds
(Sum (p | k)) + (Sum (q | k)) = n * k ) & ( for k being Nat st k in len p holds
q . k = n - (p . k) ) )
thus len p = len q by A4; :: thesis: ( rng q c= {0,n} & ( for k being Nat st k <= len p holds
(Sum (p | k)) + (Sum (q | k)) = n * k ) & ( for k being Nat st k in len p holds
q . k = n - (p . k) ) )
thus rng q c= {0,n} by RELAT_1:def 19; :: thesis: ( ( for k being Nat st k <= len p holds
(Sum (p | k)) + (Sum (q | k)) = n * k ) & ( for k being Nat st k in len p holds
q . k = n - (p . k) ) )
A19: S2[ 0 ] ;
for k being Nat holds S2[k] from NAT_1:sch 2(A19, A5);
 hence ( ( for k being Nat st k <= len p holds
(Sum (p | k)) + (Sum (q | k)) = n * k ) & ( for k being Nat st k in len p holds
q . k = n - (p . k) ) ) by A4; :: thesis: verum