let n be Nat; :: thesis: ( n > 0 implies card { [(i + 1),i] where i is Element of NAT : i + 1 < n } = n - 1 )
deffunc H1( Element of NAT ) -> object = [(\$1 + 1),\$1];
defpred S1[ Element of NAT ] means \$1 + 1 < n;
defpred S2[ Element of NAT ] means \$1 in Segm (n -' 1);
A1: for d1, d2 being Element of NAT st H1(d1) = H1(d2) holds
d1 = d2 by XTUPLE_0:1;
assume A2: n > 0 ; :: thesis: card { [(i + 1),i] where i is Element of NAT : i + 1 < n } = 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
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 ;
then i < n - 1 by ;
hence i + 1 < n by XREAL_1:20; :: thesis: verum
end;
A6: for i being Element of NAT holds
( S1[i] iff S2[i] )
proof
let i be Element of NAT ; :: thesis: ( S1[i] iff S2[i] )
thus ( i + 1 < n implies i in Segm (n -' 1) ) :: thesis: ( S2[i] implies S1[i] )
proof
assume i + 1 < n ; :: thesis: i in Segm (n -' 1)
then i < n - 1 by XREAL_1:20;
then i < n -' 1 by ;
hence i in Segm (n -' 1) by NAT_1:44; :: thesis: verum
end;
thus ( S2[i] implies S1[i] ) by A4; :: thesis: verum
end;
A7: { H1(i) where i is Element of NAT : S1[i] } = { H1(i) where i is Element of NAT : S2[i] } from A8: n -' 1 c= NAT ;
n -' 1, { H1(i) where i is Element of NAT : i in n -' 1 } are_equipotent from hence card { [(i + 1),i] where i is Element of NAT : i + 1 < n } = card (n -' 1) by
.= n -' 1
.= n - 1 by ;
:: thesis: verum