defpred S₁[ Nat] means for i being Nat st i in dom (Sgm0 ($1 /\ OddNAT)) holds
(Sgm0 ($1 /\ OddNAT)) . i = (2 * i) + 1;
A1: S₁[ 0 ]

proof

let i be Nat; :: thesis: ( i in dom (Sgm0 (0 /\ OddNAT)) implies (Sgm0 (0 /\ OddNAT)) . i = (2 * i) + 1 )
assume i in dom (Sgm0 (0 /\ OddNAT)) ; :: thesis: (Sgm0 (0 /\ OddNAT)) . i = (2 * i) + 1
then i in len (Sgm0 {}) ;
then i in card {} by AFINSQ_2:20;
hence (Sgm0 (0 /\ OddNAT)) . i = (2 * i) + 1 ; :: thesis: verum

end;

A2: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

let i be Nat; :: thesis: ( i in dom (Sgm0 ((n + 1) /\ OddNAT)) implies (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1 )
assume A4: i in dom (Sgm0 ((n + 1) /\ OddNAT)) ; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

per cases ( n is odd or n is even ) ;

suppose A5: n is odd ; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

A6: (n + 1) /\ OddNAT = (n /\ OddNAT) \/ {n}

proof

thus (n + 1) /\ OddNAT c= (n /\ OddNAT) \/ {n} :: according to XBOOLE_0:def 10 :: thesis: (n /\ OddNAT) \/ {n} c= (n + 1) /\ OddNAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (n + 1) /\ OddNAT or x in (n /\ OddNAT) \/ {n} )
assume A7: x in (n + 1) /\ OddNAT ; :: thesis: x in (n /\ OddNAT) \/ {n}
then ( x in n + 1 & x in OddNAT ) by XBOOLE_0:def 4;
then consider y being Nat such that
A8: ( y = x & y is odd ) ;
( y in Segm (n + 1) & y in OddNAT ) by A7, XBOOLE_0:def 4, A8;
then ( ( y < n or y = n ) & y in OddNAT ) by NAT_1:44, NAT_1:22;
then ( ( y in Segm n & y in OddNAT ) or y = n ) by NAT_1:44;
then ( y in n /\ OddNAT or y in {n} ) by XBOOLE_0:def 4, TARSKI:def 1;
hence x in (n /\ OddNAT) \/ {n} by A8, XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (n /\ OddNAT) \/ {n} or x in (n + 1) /\ OddNAT )
assume x in (n /\ OddNAT) \/ {n} ; :: thesis: x in (n + 1) /\ OddNAT

per cases then ( x in n /\ OddNAT or x in {n} ) by XBOOLE_0:def 3;

suppose A9: x in n /\ OddNAT ; :: thesis: x in (n + 1) /\ OddNAT

Segm n c= Segm (n + 1) by NAT_1:11, NAT_1:39;
then n /\ OddNAT c= (n + 1) /\ OddNAT by XBOOLE_1:26;
hence x in (n + 1) /\ OddNAT by A9; :: thesis: verum

end;

suppose x in {n} ; :: thesis: x in (n + 1) /\ OddNAT

then x = n by TARSKI:def 1;
then ( x in Segm (n + 1) & x in OddNAT ) by NAT_1:45, A5;
hence x in (n + 1) /\ OddNAT by XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

reconsider X = n /\ OddNAT as finite natural-membered set ;
reconsider Y = {n} as finite natural-membered set ;
A10: X <N< Y

proof

let a, b be Nat; :: according to AFINSQ_2:def 5 :: thesis: ( not a in X or not b in Y or not b <= a )
assume ( a in X & b in Y ) ; :: thesis: not b <= a
then ( a in Segm n & b = n ) by XBOOLE_0:def 4, TARSKI:def 1;
hence a < b by NAT_1:44; :: thesis: verum

end;

not n in n ;
then not n in n /\ OddNAT by XBOOLE_0:def 4;
then A11: card ((n + 1) /\ OddNAT) = (card (n /\ OddNAT)) + 1 by A6, CARD_2:41;
A12: i in Segm (dom (Sgm0 ((n + 1) /\ OddNAT))) by A4;
then i < len (Sgm0 ((n + 1) /\ OddNAT)) by NAT_1:44;
then i < (card (n /\ OddNAT)) + 1 by A11, AFINSQ_2:20;
then i < (len (Sgm0 X)) + 1 by AFINSQ_2:20;

per cases then ( i < len (Sgm0 X) or i = len (Sgm0 X) ) by NAT_1:22;

suppose A13: i < len (Sgm0 X) ; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

then A14: i < Segm (card (Sgm0 (n /\ OddNAT))) ;
thus (Sgm0 ((n + 1) /\ OddNAT)) . i = (Sgm0 (n /\ OddNAT)) . i by A10, A13, AFINSQ_2:29, A6
.= (2 * i) + 1 by A14, NAT_1:44, A3 ; :: thesis: verum

end;

suppose A15: i = len (Sgm0 X) ; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

then A16: (Sgm0 ((n + 1) /\ OddNAT)) . i = (Sgm0 Y) . 0 by AFINSQ_2:32, A10, A6
.= n by AFINSQ_2:22 ;
(Sgm0 ((n + 1) /\ OddNAT)) . i in rng (Sgm0 ((n + 1) /\ OddNAT)) by FUNCT_1:3, A4;
then (Sgm0 ((n + 1) /\ OddNAT)) . i in (n + 1) /\ OddNAT by AFINSQ_2:def 4;
then (Sgm0 ((n + 1) /\ OddNAT)) . i in OddNAT by XBOOLE_0:def 4;
then consider r being Nat such that
A17: ( r = (Sgm0 ((n + 1) /\ OddNAT)) . i & r is odd ) ;
consider j being Nat such that
A18: r = (2 * j) + 1 by A17, ABIAN:9;

per cases ( j < i or j = i or j > i ) by XXREAL_0:1;

suppose A19: j < i ; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

then A20: j < Segm (card (Sgm0 (n /\ OddNAT))) by A15;
j < card (Sgm0 ((n + 1) /\ OddNAT)) by A19, A12, NAT_1:44, XXREAL_0:2;
then A21: j in Segm (dom (Sgm0 ((n + 1) /\ OddNAT))) by NAT_1:44;
(Sgm0 ((n + 1) /\ OddNAT)) . j = (Sgm0 (n /\ OddNAT)) . j by A10, A19, A15, AFINSQ_2:29, A6
.= (Sgm0 ((n + 1) /\ OddNAT)) . i by A20, NAT_1:44, A3, A17, A18 ;
hence (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1 by A21, A4, FUNCT_1:def 4, A19; :: thesis: verum

end;

suppose j = i ; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

hence (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1 by A17, A18; :: thesis: verum

end;

suppose j > i ; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

then A22: 2 * i < 2 * j by XREAL_1:68;
A23: (2 * i) + 1 in OddNAT ;
( (2 * i) + 1 < n & n < n + 1 ) by A22, XREAL_1:8, A17, A18, A16, NAT_1:16;
then (2 * i) + 1 < n + 1 by XXREAL_0:2;
then (2 * i) + 1 in Segm (n + 1) by NAT_1:44;
then (2 * i) + 1 in (n + 1) /\ OddNAT by A23, XBOOLE_0:def 4;
then (2 * i) + 1 in rng (Sgm0 ((n + 1) /\ OddNAT)) by AFINSQ_2:def 4;
then consider l being object such that
A24: ( l in dom (Sgm0 ((n + 1) /\ OddNAT)) & (Sgm0 ((n + 1) /\ OddNAT)) . l = (2 * i) + 1 ) by FUNCT_1:def 3;
reconsider l = l as Element of NAT by A24;
l in Segm (dom (Sgm0 ((n + 1) /\ OddNAT))) by A24;
then l < len (Sgm0 ((n + 1) /\ OddNAT)) by NAT_1:44;
then l < (card (n /\ OddNAT)) + 1 by A11, AFINSQ_2:20;
then l < (len (Sgm0 X)) + 1 by AFINSQ_2:20;

per cases then ( l < len (Sgm0 X) or l = len (Sgm0 X) ) by NAT_1:22;

suppose A25: l < len (Sgm0 X) ; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

then A26: l < Segm (card (Sgm0 (n /\ OddNAT))) ;
(Sgm0 ((n + 1) /\ OddNAT)) . l = (Sgm0 (n /\ OddNAT)) . l by A10, A25, AFINSQ_2:29, A6
.= (2 * l) + 1 by A26, NAT_1:44, A3 ;
then (2 * i) + 1 = (2 * l) + 1 by A24;
hence (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1 by A25, A15; :: thesis: verum

end;

suppose l = len (Sgm0 X) ; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

hence (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1 by A15, A24; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose A27: n is even ; :: thesis: (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1

(n + 1) /\ OddNAT = n /\ OddNAT

proof

thus (n + 1) /\ OddNAT c= n /\ OddNAT :: according to XBOOLE_0:def 10 :: thesis: n /\ OddNAT c= (n + 1) /\ OddNAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (n + 1) /\ OddNAT or x in n /\ OddNAT )
assume x in (n + 1) /\ OddNAT ; :: thesis: x in n /\ OddNAT
then A28: ( x in Segm (n + 1) & x in OddNAT ) by XBOOLE_0:def 4;
then consider y being Nat such that
A29: ( y = x & y is odd ) ;
y < n by A28, A29, NAT_1:44, A27, NAT_1:22;
then ( y in Segm n & y in OddNAT ) by A29, NAT_1:44;
hence x in n /\ OddNAT by A29, XBOOLE_0:def 4; :: thesis: verum

end;

Segm n c= Segm (n + 1) by NAT_1:11, NAT_1:39;
hence n /\ OddNAT c= (n + 1) /\ OddNAT by XBOOLE_1:26; :: thesis: verum

end;

hence (Sgm0 ((n + 1) /\ OddNAT)) . i = (2 * i) + 1 by A4, A3; :: thesis: verum

end;

end;

end;

end;

for N being Nat holds S₁[N] from NAT_1:sch 2(A1, A2);
hence for N, i being Nat st i in dom (Sgm0 (N /\ OddNAT)) holds
(Sgm0 (N /\ OddNAT)) . i = (2 * i) + 1 ; :: thesis: verum