let k, n be Nat; :: thesis: for p being XFinSequence of NAT st p is dominated_by_0 & 2 * (Sum (p | k)) = k & k = n + 1 holds
p | k = (p | n) ^ (1 --> 1)
let p be XFinSequence of NAT ; :: thesis: ( p is dominated_by_0 & 2 * (Sum (p | k)) = k & k = n + 1 implies p | k = (p | n) ^ (1 --> 1) )
assume that
A1: p is dominated_by_0 and
A2: 2 * (Sum (p | k)) = k and
A3: k = n + 1 ; :: thesis: p | k = (p | n) ^ (1 --> 1)
reconsider q = p | k as XFinSequence of NAT ;
q . n = 1

proof

Sum (p | k) <> 0 by A2, A3;
then reconsider s = (Sum (p | k)) - 1 as Nat by NAT_1:14, NAT_1:21;
A4: q is dominated_by_0 by A1, Th6;
then A5: rng q c= {0,1} ;
(2 * s) + 1 = n by A2, A3;
then A6: ( Sum <%0%> = 0 & 2 * (Sum (q | n)) < n ) by A4, Th8, AFINSQ_2:53;
A7: len q = n + 1 by A1, A2, A3, Th11;
then A8: q = (q | n) ^ <%(q . n)%> by AFINSQ_1:56;
n < n + 1 by NAT_1:13;
then n in Segm (n + 1) by NAT_1:44;
then A9: q . n in rng q by A7, FUNCT_1:3;
assume q . n <> 1 ; :: thesis: contradiction
then q . n = 0 by A5, A9, TARSKI:def 2;
then Sum q = (Sum (q | n)) + (Sum <%0%>) by A8, AFINSQ_2:55;
hence contradiction by A2, A3, A6, NAT_1:13; :: thesis: verum

end;

then A10: ( dom <%(q . n)%> = 1 & rng <%(q . n)%> = {1} ) by AFINSQ_1:33;
n <= n + 1 by NAT_1:11;
then Segm n c= Segm k by A3, NAT_1:39;
then A11: q | n = p | n by RELAT_1:74;
len q = n + 1 by A1, A2, A3, Th11;
then q = (q | n) ^ <%(q . n)%> by AFINSQ_1:56;
hence p | k = (p | n) ^ (1 --> 1) by A11, A10, FUNCOP_1:9; :: thesis: verum