let p be XFinSequence of NAT ; 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; ( 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}
; 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]
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);
rng q c= {0,nn}
;
then
rng q c= NAT
by XBOOLE_1:1;
then reconsider q = q as XFinSequence of NAT by RELAT_1:def 19;
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;
( S2[k] implies S2[k + 1] )
assume A6:
S2[
k]
;
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
;
(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;
verum
end;
take
q
; ( 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; ( 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; ( ( 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; verum