let k, n be Element of NAT ; :: thesis: for p being XFinSequence of 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 ; :: thesis: ( p is dominated_by_0 & 2 * (Sum (p | k)) = k & k = n + 1 implies p | k = (p | n) ^ (1 --> 1) )
assume A1: ( p is dominated_by_0 & 2 * (Sum (p | k)) = k & k = n + 1 ) ; :: thesis: p | k = (p | n) ^ (1 --> 1)
set q = p | k;
n <= n + 1 by NAT_1:11;
then ( len (p | k) = n + 1 & n c= k ) by A1, Th15, NAT_1:40;
then A2: ( p | k = ((p | k) | n) ^ <%((p | k) . n)%> & (p | k) | n = p | n ) by CARD_FIN:43, RELAT_1:103;
(p | k) . n = 1

proof

assume A3: (p | k) . n <> 1 ; :: thesis: contradiction
n < n + 1 by NAT_1:13;
then A4: ( p | k is dominated_by_0 & len (p | k) = n + 1 & dom (p | k) = len (p | k) & n in n + 1 ) by A1, Th10, Th15, NAT_1:45;
then ( rng (p | k) c= {0 ,1} & (p | k) . n in rng (p | k) ) by Def1, FUNCT_1:12;
then ( (p | k) . n = 0 & p | k = ((p | k) | n) ^ <%((p | k) . n)%> ) by A3, A4, CARD_FIN:43, TARSKI:def 2;
then A5: ( Sum (p | k) = (Sum ((p | k) | n)) + (Sum <%0 %>) & Sum <%0 %> = 0 ) by Lm4, STIRL2_1:44;
Sum (p | k) <> 0 by A1;
then reconsider s = (Sum (p | k)) - 1 as Element of NAT by NAT_1:14, NAT_1:21;
(2 * s) + 1 = n by A1;
then ( 2 * (Sum ((p | k) | n)) < n & n < k ) by A1, A4, Th12, NAT_1:13;
hence contradiction by A1, A5; :: thesis: verum

end;

then ( dom <%((p | k) . n)%> = 1 & rng <%((p | k) . n)%> = {1} ) by AFINSQ_1:36;
hence p | k = (p | n) ^ (1 --> 1) by A2, FUNCOP_1:15; :: thesis: verum