let n be Nat; :: thesis: ( n > 0 implies card the InternalRel of (n -SuccRelStr) = n - 1 )

deffunc H_{1}( Element of NAT ) -> object = [$1,($1 + 1)];

defpred S_{1}[ Element of NAT ] means $1 + 1 < n;

defpred S_{2}[ set ] means $1 in Segm (n -' 1);

A1: n -' 1 c= NAT ;

assume A2: n > 0 ; :: thesis: card the InternalRel of (n -SuccRelStr) = n - 1

then A3: n >= 0 + 1 by NAT_1:13;

A4: for i being Nat st i in Segm (n -' 1) holds

i + 1 < n

( S_{1}[i] iff S_{2}[i] )
_{1}(i) where i is Element of NAT : S_{1}[i] } = { H_{1}(i) where i is Element of NAT : S_{2}[i] }
from FRAENKEL:sch 3(A6);

deffunc H_{2}( Element of NAT ) -> object = [$1,($1 + 1)];

A8: for d1, d2 being Element of NAT st H_{2}(d1) = H_{2}(d2) holds

d1 = d2 by XTUPLE_0:1;

A9: n -' 1, { H_{2}(i) where i is Element of NAT : i in n -' 1 } are_equipotent
from FUNCT_7:sch 4(A1, A8);

thus card the InternalRel of (n -SuccRelStr) = card { [i,(i + 1)] where i is Element of NAT : i + 1 < n } by Def6

.= card (n -' 1) by A7, A9, CARD_1:5

.= n -' 1

.= n - 1 by A3, XREAL_1:233 ; :: thesis: verum

deffunc H

defpred S

defpred S

A1: n -' 1 c= NAT ;

assume A2: n > 0 ; :: thesis: card the InternalRel of (n -SuccRelStr) = n - 1

then A3: n >= 0 + 1 by NAT_1:13;

A4: for i being Nat st i in Segm (n -' 1) holds

i + 1 < n

proof

A6:
for i being Element of NAT holds
let i be Nat; :: thesis: ( i in Segm (n -' 1) implies i + 1 < n )

assume i in Segm (n -' 1) ; :: thesis: i + 1 < n

then A5: i < n -' 1 by NAT_1:44;

n >= 0 + 1 by A2, NAT_1:13;

then i < n - 1 by A5, XREAL_1:233;

hence i + 1 < n by XREAL_1:20; :: thesis: verum

end;assume i in Segm (n -' 1) ; :: thesis: i + 1 < n

then A5: i < n -' 1 by NAT_1:44;

n >= 0 + 1 by A2, NAT_1:13;

then i < n - 1 by A5, XREAL_1:233;

hence i + 1 < n by XREAL_1:20; :: thesis: verum

( S

proof

A7:
{ H
let i be Element of NAT ; :: thesis: ( S_{1}[i] iff S_{2}[i] )

thus ( i + 1 < n implies i in Segm (n -' 1) ) :: thesis: ( S_{2}[i] implies S_{1}[i] )_{2}[i] implies S_{1}[i] )
by A4; :: thesis: verum

end;thus ( i + 1 < n implies i in Segm (n -' 1) ) :: thesis: ( S

proof

thus
( S
assume
i + 1 < n
; :: thesis: i in Segm (n -' 1)

then i < n - 1 by XREAL_1:20;

then i < n -' 1 by A3, XREAL_1:233;

hence i in Segm (n -' 1) by NAT_1:44; :: thesis: verum

end;then i < n - 1 by XREAL_1:20;

then i < n -' 1 by A3, XREAL_1:233;

hence i in Segm (n -' 1) by NAT_1:44; :: thesis: verum

deffunc H

A8: for d1, d2 being Element of NAT st H

d1 = d2 by XTUPLE_0:1;

A9: n -' 1, { H

thus card the InternalRel of (n -SuccRelStr) = card { [i,(i + 1)] where i is Element of NAT : i + 1 < n } by Def6

.= card (n -' 1) by A7, A9, CARD_1:5

.= n -' 1

.= n - 1 by A3, XREAL_1:233 ; :: thesis: verum