let p, q be XFinSequence of NAT ; :: thesis: for k being Nat st p | ((2 * k) + (len q)) = ((k --> 0) ^ q) ^ (k --> 1) & q is dominated_by_0 & 2 * (Sum q) = len q & k > 0 holds
min* { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } = (2 * k) + (len q)
let k be Nat; :: thesis: ( p | ((2 * k) + (len q)) = ((k --> 0) ^ q) ^ (k --> 1) & q is dominated_by_0 & 2 * (Sum q) = len q & k > 0 implies min* { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } = (2 * k) + (len q) )
assume that
A1: p | ((2 * k) + (len q)) = ((k --> 0) ^ q) ^ (k --> 1) and
A2: q is dominated_by_0 and
A3: 2 * (Sum q) = len q and
A4: k > 0 ; :: thesis: min* { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } = (2 * k) + (len q)
set k0 = k --> 0;
A5: Sum (k --> 0) = k * 0 by AFINSQ_2:58;
then A6: 2 * k > 0 by A4, XREAL_1:68;
reconsider k1 = k --> 1 as XFinSequence of NAT ;
set M = { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } ;
set kqk = ((k --> 0) ^ q) ^ k1;
Sum (((k --> 0) ^ q) ^ k1) = (Sum ((k --> 0) ^ q)) + (Sum k1) by AFINSQ_2:55;
then A7: Sum (((k --> 0) ^ q) ^ k1) = ((Sum (k --> 0)) + (Sum q)) + (Sum k1) by AFINSQ_2:55;
Sum k1 = k * 1 by AFINSQ_2:58;
then 2 * (Sum (p | ((2 * k) + (len q)))) = (len q) + (2 * k) by A1, A3, A7, A5;
then A8: (2 * k) + (len q) in { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } by A6;
{ N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } or y in NAT )
assume y in { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } ; :: thesis: y in NAT
then ex i being Nat st
( i = y & 2 * (Sum (p | i)) = i & i > 0 ) ;
hence y in NAT by ORDINAL1:def 12; :: thesis: verum

end;

then reconsider M = { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } as non empty Subset of NAT by A8;
min* M = (2 * k) + (len q)

proof

((k --> 0) ^ q) ^ k1 = (k --> 0) ^ (q ^ k1) by AFINSQ_1:27;
then A9: len (((k --> 0) ^ q) ^ k1) = (len (k --> 0)) + (len (q ^ k1)) by AFINSQ_1:17;
A10: len (((k --> 0) ^ q) ^ k1) = k + ((len q) + (len k1)) by A9, AFINSQ_1:17;
assume A11: min* M <> (2 * k) + (len q) ; :: thesis: contradiction
min* M in M by NAT_1:def 1;
then A12: ex i being Nat st
( i = min* M & 2 * (Sum (p | i)) = i & i > 0 ) ;
A14: (2 * k) + (len q) >= min* M by A8, NAT_1:def 1;
then A15: Segm (min* M) c= Segm ((2 * k) + (len q)) by NAT_1:39;
then A16: p | (min* M) = (((k --> 0) ^ q) ^ k1) | (min* M) by A1, RELAT_1:74;

now :: thesis: contradiction

per cases ( min* M <= k or min* M > k ) ;

suppose A17: min* M <= k ; :: thesis: contradiction

( k = dom (k --> 0) & ((k --> 0) ^ q) ^ k1 = (k --> 0) ^ (q ^ k1) ) by AFINSQ_1:27;
then A18: (((k --> 0) ^ q) ^ k1) | (min* M) = (k --> 0) | (min* M) by A17, AFINSQ_1:58;
A19: Sum ((min* M) --> 0) = (min* M) * 0 by AFINSQ_2:58;
(k --> 0) | (min* M) = (min* M) --> 0 by A17, Lm1;
then Sum (p | (min* M)) = Sum ((min* M) --> 0) by A1, A15, A18, RELAT_1:74;
hence contradiction by A12, A19; :: thesis: verum

end;

suppose min* M > k ; :: thesis: contradiction

then reconsider mk = (min* M) - k as Nat by NAT_1:21;

now :: thesis: contradiction

per cases ( min* M <= k + (len q) or min* M > k + (len q) ) ;

suppose A20: min* M <= k + (len q) ; :: thesis: contradiction

A21: dom (k --> 0) = k ;
min* M = mk + k ;
then A22: ((k --> 0) ^ q) | (min* M) = (k --> 0) ^ (q | mk) by A21, AFINSQ_1:59;
dom ((k --> 0) ^ q) = (len (k --> 0)) + (len q) by AFINSQ_1:def 3;
then (((k --> 0) ^ q) ^ k1) | (min* M) = ((k --> 0) ^ q) | (min* M) by A20, AFINSQ_1:58;
then A23: Sum (p | (min* M)) = (Sum (k --> 0)) + (Sum (q | mk)) by A16, A22, AFINSQ_2:55;
A24: 1 <= k by A4, NAT_1:14;
Sum (k --> 0) = k * 0 by AFINSQ_2:58;
then mk + k <= mk by A2, A12, A23, Th2;
hence contradiction by A24, NAT_1:19; :: thesis: verum

end;

suppose min* M > k + (len q) ; :: thesis: contradiction

then reconsider mkL = (min* M) - (k + (len q)) as Nat by NAT_1:21;
A25: 2 * (Sum (p | (min* M))) = min* M by A12;
( dom ((k --> 0) ^ q) = (len (k --> 0)) + (len q) & dom (k --> 0) = k ) by AFINSQ_1:def 3;
then min* M = (dom ((k --> 0) ^ q)) + mkL ;
then (((k --> 0) ^ q) ^ k1) | (min* M) = ((k --> 0) ^ q) ^ (k1 | mkL) by AFINSQ_1:59;
then A26: Sum (p | (min* M)) = (Sum ((k --> 0) ^ q)) + (Sum (k1 | mkL)) by A16, AFINSQ_2:55;
min* M < len (((k --> 0) ^ q) ^ k1) by A11, A10, A14, XXREAL_0:1;
then mkL < ((2 * k) + (len q)) - (k + (len q)) by A10, XREAL_1:9;
then k1 | mkL = mkL --> 1 by Lm1;
then A27: Sum (k1 | mkL) = mkL * 1 by AFINSQ_2:58;
( Sum ((k --> 0) ^ q) = (Sum (k --> 0)) + (Sum q) & Sum (k --> 0) = k * 0 ) by AFINSQ_2:55, AFINSQ_2:58;
hence contradiction by A3, A11, A26, A27, A25; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence min* { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } = (2 * k) + (len q) ; :: thesis: verum