let p be XFinSequence of ; :: thesis:
let n be Element of NAT ; :: thesis:
assume A1: rng p c= {0 ,n} ; :: thesis:
defpred S₁[ set , set ] means for k being Element of NAT st k = $1 holds
$2 = n - (p . k);
A2: for k being Element of NAT st k in len p holds
ex x being Element of {0 ,n} st S₁[k,x]

let k be Element of NAT ; :: thesis:
assume A3: k in len p ; :: thesis:
k in dom p by A3;
then p . k in rng p by FUNCT_1:12;
then ( p . k = 0 or p . k = n ) by A1, TARSKI:def 2;
then ( n - (p . k) in {0 ,n} & S₁[k,n - (p . k)] ) by TARSKI:def 2;
hence ex x being Element of {0 ,n} st S₁[k,x] ; :: thesis:

end;

consider q being XFinSequence of such that
A4: ( dom q = len p & ( for k being Element of NAT st k in len p holds
S₁[k,q . k] ) ) from STIRL2_1:sch 6(A2);
( rng q c= {0 ,n} & {0 ,n} is Subset of NAT ) by RELAT_1:def 19;
then rng q c= NAT by XBOOLE_1:1;
then reconsider q = q as XFinSequence of by RELAT_1:def 19;
take q ; :: thesis:
thus len p = len q by A4; :: thesis:
thus rng q c= {0 ,n} by RELAT_1:def 19; :: thesis:
defpred S₂[ Element of NAT ] means ( $1 <= len p implies (Sum (p | $1)) + (Sum (q | $1)) = n * $1 );
A5: S₂[ 0 ]

assume 0 <= len p ; :: thesis:
( len {} = 0 & p | 0 = {} & q | 0 = {} & the_unity_wrt addnat = 0 ) by BINOP_2:5;
then ( addnat "**" (p | 0 ) = 0 & addnat "**" (q | 0 ) = 0 ) by STIRL2_1:def 3;
hence (Sum (p | 0 )) + (Sum (q | 0 )) = n * 0 ; :: thesis:

end;

A6: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

end;

for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A5, A6);
hence ( ( for k being Element of NAT st k <= len p holds
(Sum (p | k)) + (Sum (q | k)) = n * k ) & ( for k being Element of NAT st k in len p holds
q . k = n - (p . k) ) ) by A4; :: thesis: