defpred S_{1}[ Nat] means for i being Nat st i in dom (Sgm0 ($1 /\ EvenNAT)) holds

(Sgm0 ($1 /\ EvenNAT)) . i = 2 * i;

A1: S_{1}[ 0 ]
_{1}[N]
from NAT_1:sch 2(A1, A2);

hence for N, i being Nat st i in dom (Sgm0 (N /\ EvenNAT)) holds

(Sgm0 (N /\ EvenNAT)) . i = 2 * i ; :: thesis: verum

(Sgm0 ($1 /\ EvenNAT)) . i = 2 * i;

A1: S

proof

let i be Nat; :: thesis: ( i in dom (Sgm0 (0 /\ EvenNAT)) implies (Sgm0 (0 /\ EvenNAT)) . i = 2 * i )

assume i in dom (Sgm0 (0 /\ EvenNAT)) ; :: thesis: (Sgm0 (0 /\ EvenNAT)) . i = 2 * i

then i in len (Sgm0 {}) ;

then i in card {} by AFINSQ_2:20;

hence (Sgm0 (0 /\ EvenNAT)) . i = 2 * i ; :: thesis: verum

end;assume i in dom (Sgm0 (0 /\ EvenNAT)) ; :: thesis: (Sgm0 (0 /\ EvenNAT)) . i = 2 * i

then i in len (Sgm0 {}) ;

then i in card {} by AFINSQ_2:20;

hence (Sgm0 (0 /\ EvenNAT)) . i = 2 * i ; :: thesis: verum

A2: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

for N being Nat holds SS

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[n + 1]

thus S_{1}[n + 1]
:: thesis: verum

end;assume A3: S

thus S

proof

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

assume A4: i in dom (Sgm0 ((n + 1) /\ EvenNAT)) ; :: thesis: (Sgm0 ((n + 1) /\ EvenNAT)) . i = 2 * i

end;assume A4: i in dom (Sgm0 ((n + 1) /\ EvenNAT)) ; :: thesis: (Sgm0 ((n + 1) /\ EvenNAT)) . i = 2 * i

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

end;

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

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

reconsider Y = {n} as finite natural-membered set ;

A10: X <N< Y

then not n in n /\ EvenNAT by XBOOLE_0:def 4;

then A11: card ((n + 1) /\ EvenNAT) = (card (n /\ EvenNAT)) + 1 by A6, CARD_2:41;

A12: i in Segm (dom (Sgm0 ((n + 1) /\ EvenNAT))) by A4;

then i < len (Sgm0 ((n + 1) /\ EvenNAT)) by NAT_1:44;

then i < (card (n /\ EvenNAT)) + 1 by A11, AFINSQ_2:20;

then i < (len (Sgm0 X)) + 1 by AFINSQ_2:20;

end;proof

reconsider X = n /\ EvenNAT as finite natural-membered set ;
thus
(n + 1) /\ EvenNAT c= (n /\ EvenNAT) \/ {n}
:: according to XBOOLE_0:def 10 :: thesis: (n /\ EvenNAT) \/ {n} c= (n + 1) /\ EvenNAT

assume x in (n /\ EvenNAT) \/ {n} ; :: thesis: x in (n + 1) /\ EvenNAT

end;proof

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

assume A7: x in (n + 1) /\ EvenNAT ; :: thesis: x in (n /\ EvenNAT) \/ {n}

then ( x in n + 1 & x in EvenNAT ) by XBOOLE_0:def 4;

then consider y being Nat such that

A8: ( y = x & y is even ) ;

( y in Segm (n + 1) & y in EvenNAT ) by A7, XBOOLE_0:def 4, A8;

then ( ( y < n or y = n ) & y in EvenNAT ) by NAT_1:44, NAT_1:22;

then ( ( y in Segm n & y in EvenNAT ) or y = n ) by NAT_1:44;

then ( y in n /\ EvenNAT or y in {n} ) by XBOOLE_0:def 4, TARSKI:def 1;

hence x in (n /\ EvenNAT) \/ {n} by A8, XBOOLE_0:def 3; :: thesis: verum

end;assume A7: x in (n + 1) /\ EvenNAT ; :: thesis: x in (n /\ EvenNAT) \/ {n}

then ( x in n + 1 & x in EvenNAT ) by XBOOLE_0:def 4;

then consider y being Nat such that

A8: ( y = x & y is even ) ;

( y in Segm (n + 1) & y in EvenNAT ) by A7, XBOOLE_0:def 4, A8;

then ( ( y < n or y = n ) & y in EvenNAT ) by NAT_1:44, NAT_1:22;

then ( ( y in Segm n & y in EvenNAT ) or y = n ) by NAT_1:44;

then ( y in n /\ EvenNAT or y in {n} ) by XBOOLE_0:def 4, TARSKI:def 1;

hence x in (n /\ EvenNAT) \/ {n} by A8, XBOOLE_0:def 3; :: thesis: verum

assume x in (n /\ EvenNAT) \/ {n} ; :: thesis: x in (n + 1) /\ EvenNAT

reconsider Y = {n} as finite natural-membered set ;

A10: X <N< Y

proof

not n in n
;
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;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

then not n in n /\ EvenNAT by XBOOLE_0:def 4;

then A11: card ((n + 1) /\ EvenNAT) = (card (n /\ EvenNAT)) + 1 by A6, CARD_2:41;

A12: i in Segm (dom (Sgm0 ((n + 1) /\ EvenNAT))) by A4;

then i < len (Sgm0 ((n + 1) /\ EvenNAT)) by NAT_1:44;

then i < (card (n /\ EvenNAT)) + 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;

end;

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

then A14:
i < Segm (card (Sgm0 (n /\ EvenNAT)))
;

thus (Sgm0 ((n + 1) /\ EvenNAT)) . i = (Sgm0 (n /\ EvenNAT)) . i by A10, A13, AFINSQ_2:29, A6

.= 2 * i by A14, NAT_1:44, A3 ; :: thesis: verum

end;thus (Sgm0 ((n + 1) /\ EvenNAT)) . i = (Sgm0 (n /\ EvenNAT)) . i by A10, A13, AFINSQ_2:29, A6

.= 2 * i by A14, NAT_1:44, A3 ; :: thesis: verum

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

then A16: (Sgm0 ((n + 1) /\ EvenNAT)) . i =
(Sgm0 Y) . 0
by AFINSQ_2:32, A10, A6

.= n by AFINSQ_2:22 ;

(Sgm0 ((n + 1) /\ EvenNAT)) . i in rng (Sgm0 ((n + 1) /\ EvenNAT)) by FUNCT_1:3, A4;

then (Sgm0 ((n + 1) /\ EvenNAT)) . i in (n + 1) /\ EvenNAT by AFINSQ_2:def 4;

then (Sgm0 ((n + 1) /\ EvenNAT)) . i in EvenNAT by XBOOLE_0:def 4;

then consider r being Nat such that

A17: ( r = (Sgm0 ((n + 1) /\ EvenNAT)) . i & r is even ) ;

consider j being Nat such that

A18: r = 2 * j by A17, ABIAN:def 2;

end;.= n by AFINSQ_2:22 ;

(Sgm0 ((n + 1) /\ EvenNAT)) . i in rng (Sgm0 ((n + 1) /\ EvenNAT)) by FUNCT_1:3, A4;

then (Sgm0 ((n + 1) /\ EvenNAT)) . i in (n + 1) /\ EvenNAT by AFINSQ_2:def 4;

then (Sgm0 ((n + 1) /\ EvenNAT)) . i in EvenNAT by XBOOLE_0:def 4;

then consider r being Nat such that

A17: ( r = (Sgm0 ((n + 1) /\ EvenNAT)) . i & r is even ) ;

consider j being Nat such that

A18: r = 2 * j by A17, ABIAN:def 2;

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

end;

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

then A20:
j < Segm (card (Sgm0 (n /\ EvenNAT)))
by A15;

j < card (Sgm0 ((n + 1) /\ EvenNAT)) by A19, A12, NAT_1:44, XXREAL_0:2;

then A21: j in Segm (dom (Sgm0 ((n + 1) /\ EvenNAT))) by NAT_1:44;

(Sgm0 ((n + 1) /\ EvenNAT)) . j = (Sgm0 (n /\ EvenNAT)) . j by A10, A19, A15, AFINSQ_2:29, A6

.= (Sgm0 ((n + 1) /\ EvenNAT)) . i by A20, NAT_1:44, A3, A17, A18 ;

hence (Sgm0 ((n + 1) /\ EvenNAT)) . i = 2 * i by A21, A4, FUNCT_1:def 4, A19; :: thesis: verum

end;j < card (Sgm0 ((n + 1) /\ EvenNAT)) by A19, A12, NAT_1:44, XXREAL_0:2;

then A21: j in Segm (dom (Sgm0 ((n + 1) /\ EvenNAT))) by NAT_1:44;

(Sgm0 ((n + 1) /\ EvenNAT)) . j = (Sgm0 (n /\ EvenNAT)) . j by A10, A19, A15, AFINSQ_2:29, A6

.= (Sgm0 ((n + 1) /\ EvenNAT)) . i by A20, NAT_1:44, A3, A17, A18 ;

hence (Sgm0 ((n + 1) /\ EvenNAT)) . i = 2 * i by A21, A4, FUNCT_1:def 4, A19; :: thesis: verum

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

A23:
2 * i in EvenNAT
;

( 2 * i < n & n < n + 1 ) by A22, XREAL_1:68, A17, A18, A16, NAT_1:16;

then 2 * i < n + 1 by XXREAL_0:2;

then 2 * i in Segm (n + 1) by NAT_1:44;

then 2 * i in (n + 1) /\ EvenNAT by A23, XBOOLE_0:def 4;

then 2 * i in rng (Sgm0 ((n + 1) /\ EvenNAT)) by AFINSQ_2:def 4;

then consider l being object such that

A24: ( l in dom (Sgm0 ((n + 1) /\ EvenNAT)) & (Sgm0 ((n + 1) /\ EvenNAT)) . l = 2 * i ) by FUNCT_1:def 3;

reconsider l = l as Element of NAT by A24;

l in Segm (dom (Sgm0 ((n + 1) /\ EvenNAT))) by A24;

then l < len (Sgm0 ((n + 1) /\ EvenNAT)) by NAT_1:44;

then l < (card (n /\ EvenNAT)) + 1 by A11, AFINSQ_2:20;

then l < (len (Sgm0 X)) + 1 by AFINSQ_2:20;

end;( 2 * i < n & n < n + 1 ) by A22, XREAL_1:68, A17, A18, A16, NAT_1:16;

then 2 * i < n + 1 by XXREAL_0:2;

then 2 * i in Segm (n + 1) by NAT_1:44;

then 2 * i in (n + 1) /\ EvenNAT by A23, XBOOLE_0:def 4;

then 2 * i in rng (Sgm0 ((n + 1) /\ EvenNAT)) by AFINSQ_2:def 4;

then consider l being object such that

A24: ( l in dom (Sgm0 ((n + 1) /\ EvenNAT)) & (Sgm0 ((n + 1) /\ EvenNAT)) . l = 2 * i ) by FUNCT_1:def 3;

reconsider l = l as Element of NAT by A24;

l in Segm (dom (Sgm0 ((n + 1) /\ EvenNAT))) by A24;

then l < len (Sgm0 ((n + 1) /\ EvenNAT)) by NAT_1:44;

then l < (card (n /\ EvenNAT)) + 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;

end;

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

then A26:
l < Segm (card (Sgm0 (n /\ EvenNAT)))
;

(Sgm0 ((n + 1) /\ EvenNAT)) . l = (Sgm0 (n /\ EvenNAT)) . l by A10, A25, AFINSQ_2:29, A6

.= 2 * l by A26, NAT_1:44, A3 ;

then 2 * i = 2 * l by A24;

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

end;(Sgm0 ((n + 1) /\ EvenNAT)) . l = (Sgm0 (n /\ EvenNAT)) . l by A10, A25, AFINSQ_2:29, A6

.= 2 * l by A26, NAT_1:44, A3 ;

then 2 * i = 2 * l by A24;

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

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

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

end;proof

hence
(Sgm0 ((n + 1) /\ EvenNAT)) . i = 2 * i
by A4, A3; :: thesis: verum
thus
(n + 1) /\ EvenNAT c= n /\ EvenNAT
:: according to XBOOLE_0:def 10 :: thesis: n /\ EvenNAT c= (n + 1) /\ EvenNAT

hence n /\ EvenNAT c= (n + 1) /\ EvenNAT by XBOOLE_1:26; :: thesis: verum

end;proof

Segm n c= Segm (n + 1)
by NAT_1:11, NAT_1:39;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (n + 1) /\ EvenNAT or x in n /\ EvenNAT )

assume x in (n + 1) /\ EvenNAT ; :: thesis: x in n /\ EvenNAT

then A28: ( x in Segm (n + 1) & x in EvenNAT ) by XBOOLE_0:def 4;

then consider y being Nat such that

A29: ( y = x & y is even ) ;

y < n by A28, A29, NAT_1:44, A27, NAT_1:22;

then ( y in Segm n & y in EvenNAT ) by A29, NAT_1:44;

hence x in n /\ EvenNAT by A29, XBOOLE_0:def 4; :: thesis: verum

end;assume x in (n + 1) /\ EvenNAT ; :: thesis: x in n /\ EvenNAT

then A28: ( x in Segm (n + 1) & x in EvenNAT ) by XBOOLE_0:def 4;

then consider y being Nat such that

A29: ( y = x & y is even ) ;

y < n by A28, A29, NAT_1:44, A27, NAT_1:22;

then ( y in Segm n & y in EvenNAT ) by A29, NAT_1:44;

hence x in n /\ EvenNAT by A29, XBOOLE_0:def 4; :: thesis: verum

hence n /\ EvenNAT c= (n + 1) /\ EvenNAT by XBOOLE_1:26; :: thesis: verum

hence for N, i being Nat st i in dom (Sgm0 (N /\ EvenNAT)) holds

(Sgm0 (N /\ EvenNAT)) . i = 2 * i ; :: thesis: verum