let k, n be Element of 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)
set q = p | k;
(p | k) . n = 1

proof

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

end;

then A9: ( dom <%((p | k) . n)%> = 1 & rng <%((p | k) . n)%> = {1} ) by AFINSQ_1:36;
n <= n + 1 by NAT_1:11;
then n c= k by A3, NAT_1:40;
then A10: (p | k) | n = p | n by RELAT_1:103;
len (p | k) = n + 1 by A1, A2, A3, Th15;
then p | k = ((p | k) | n) ^ <%((p | k) . n)%> by CARD_FIN:43;
hence p | k = (p | n) ^ (1 --> 1) by A10, A9, FUNCOP_1:15; :: thesis: verum