let k, n be Nat; 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 ; ( 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
; p | k = (p | n) ^ (1 --> 1)
reconsider q = p | k as XFinSequence of ;
q . 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;
W:
q is
dominated_by_0
by A1, Th10;
then A4:
rng q c= {0,1}
by Def1;
(2 * s) + 1
= n
by A2, A3;
then A5:
(
Sum <%0%> = 0 & 2
* (Sum (q | n)) < n )
by W, Th12, AFINSQ_2:65;
A6:
len q = n + 1
by A1, A2, A3, Th15;
then A7:
q = (q | n) ^ <%(q . n)%>
by AFINSQ_1:60;
n < n + 1
by NAT_1:13;
then
n in n + 1
by NAT_1:45;
then A8:
q . n in rng q
by A6, FUNCT_1:12;
assume
q . n <> 1
;
contradiction
then
q . n = 0
by A4, A8, TARSKI:def 2;
then
Sum q = (Sum (q | n)) + (Sum <%0%>)
by A7, AFINSQ_2:67;
hence
contradiction
by A2, A3, A5, NAT_1:13;
verum
end;
then A9:
( dom <%(q . n)%> = 1 & rng <%(q . n)%> = {1} )
by AFINSQ_1:36;
n <= n + 1
by NAT_1:11;
then
n c= k
by A3, NAT_1:40;
then A10:
q | n = p | n
by RELAT_1:103;
len q = n + 1
by A1, A2, A3, Th15;
then
q = (q | n) ^ <%(q . n)%>
by AFINSQ_1:60;
hence
p | k = (p | n) ^ (1 --> 1)
by A10, A9, FUNCOP_1:15; verum