let n be Nat; :: thesis: ( n > 0 implies card the InternalRel of () = 2 * (n - 1) )
deffunc H1( Element of NAT ) -> Element of omega = \$1 + 1;
deffunc H2( Element of NAT ) -> Element of NAT = \$1;
defpred S1[ Element of NAT ] means \$1 + 1 < n;
set A = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ;
set B = { [H1(i),H2(i)] where i is Element of NAT : S1[i] } ;
A1: { [i,(i + 1)] where i is Element of NAT : i + 1 < n } is Relation-like
proof
let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } or ex b1, b2 being object st x = [b1,b2] )
assume x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ; :: thesis: ex b1, b2 being object st x = [b1,b2]
then ex i being Element of NAT st
( x = [i,(i + 1)] & i + 1 < n ) ;
hence ex b1, b2 being object st x = [b1,b2] ; :: thesis: verum
end;
A2: the InternalRel of () = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [H1(i),H2(i)] where i is Element of NAT : S1[i] } by Th17;
assume A3: n > 0 ; :: thesis: card the InternalRel of () = 2 * (n - 1)
then n >= 0 + 1 by NAT_1:13;
then A4: n -' 1 = n - 1 by XREAL_1:233;
{ [i,(i + 1)] where i is Element of NAT : i + 1 < n } = the InternalRel of () by Def6;
then A5: card { [i,(i + 1)] where i is Element of NAT : i + 1 < n } = n - 1 by ;
reconsider A = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } as Relation by A1;
A6: A = { [H2(i),H1(i)] where i is Element of NAT : S1[i] } ;
A7: A ~ = { [H1(i),H2(i)] where i is Element of NAT : S1[i] } from A8: A misses { [H1(i),H2(i)] where i is Element of NAT : S1[i] }
proof
assume A meets { [H1(i),H2(i)] where i is Element of NAT : S1[i] } ; :: thesis: contradiction
then consider x being object such that
A9: x in A and
A10: x in { [H1(i),H2(i)] where i is Element of NAT : S1[i] } by XBOOLE_0:3;
consider y, z being object such that
A11: x = [y,z] by ;
[z,y] in A by ;
then consider j being Element of NAT such that
A12: [z,y] = [j,(j + 1)] and
j + 1 < n ;
A13: ( z = j & y = j + 1 ) by ;
consider i being Element of NAT such that
A14: [y,z] = [i,(i + 1)] and
i + 1 < n by ;
( y = i & z = i + 1 ) by ;
hence contradiction by A13; :: thesis: verum
end;
card { [H1(i),H2(i)] where i is Element of NAT : S1[i] } = n - 1 by ;
then card the InternalRel of () = (card (n - 1)) +` (card (n - 1)) by
.= card ((n -' 1) + (n -' 1)) by
.= 2 * (n - 1) by A4 ;
hence card the InternalRel of () = 2 * (n - 1) ; :: thesis: verum