let k, n be Nat; 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 ; ( 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 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
;
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;
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; verum