let m be positive Nat; :: thesis: card { [x,y] where x, y is positive Nat : x + y = m + 1 } = m
set A = { [x,y] where x, y is positive Nat : x + y = m + 1 } ;
A1: Seg m, { [x,y] where x, y is positive Nat : x + y = m + 1 } are_equipotent

proof

defpred S₁[ object , object ] means ex k being Nat st
( k = $1 & $2 = [k,((m - k) + 1)] );
A2: for e being object st e in Seg m holds
ex u being object st S₁[e,u]

proof

let e be object ; :: thesis: ( e in Seg m implies ex u being object st S₁[e,u] )
assume e in Seg m ; :: thesis: ex u being object st S₁[e,u]
then reconsider e = e as Nat ;
take [e,((m - e) + 1)] ; :: thesis: S₁[e,[e,((m - e) + 1)]]
take e ; :: thesis: ( e = e & [e,((m - e) + 1)] = [e,((m - e) + 1)] )
thus ( e = e & [e,((m - e) + 1)] = [e,((m - e) + 1)] ) ; :: thesis: verum

end;

consider f being Function such that
A3: dom f = Seg m and
A4: for e being object st e in Seg m holds
S₁[e,f . e] from CLASSES1:sch 1(A2);
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = Seg m & proj2 f = { [x,y] where x, y is positive Nat : x + y = m + 1 } )
thus f is one-to-one :: thesis: ( proj1 f = Seg m & proj2 f = { [x,y] where x, y is positive Nat : x + y = m + 1 } )

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A5: ( x1 in dom f & x2 in dom f ) and
A6: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of NAT by A3, A5;
( S₁[x1,f . x1] & S₁[x2,f . x2] ) by A3, A4, A5;
hence x1 = x2 by A6, XTUPLE_0:1; :: thesis: verum

end;

thus dom f = Seg m by A3; :: thesis: proj2 f = { [x,y] where x, y is positive Nat : x + y = m + 1 }
thus rng f c= { [x,y] where x, y is positive Nat : x + y = m + 1 } :: according to XBOOLE_0:def 10 :: thesis: { [x,y] where x, y is positive Nat : x + y = m + 1 } c= proj2 f

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng f or b in { [x,y] where x, y is positive Nat : x + y = m + 1 } )
assume b in rng f ; :: thesis: b in { [x,y] where x, y is positive Nat : x + y = m + 1 }
then consider a being object such that
A7: a in dom f and
A8: f . a = b by FUNCT_1:def 3;
consider k being Nat such that
A9: k = a and
A10: f . a = [k,((m - k) + 1)] by A3, A4, A7;
A11: 1 <= k by A3, A7, A9, FINSEQ_1:1;
k <= m by A3, A7, A9, FINSEQ_1:1;
then m - k >= m - m by XREAL_1:10;
then A12: (m - k) + 1 is positive Element of NAT by INT_1:3;
k + ((m - k) + 1) = m + 1 ;
hence b in { [x,y] where x, y is positive Nat : x + y = m + 1 } by A8, A10, A11, A12; :: thesis: verum

end;

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { [x,y] where x, y is positive Nat : x + y = m + 1 } or b in proj2 f )
assume b in { [x,y] where x, y is positive Nat : x + y = m + 1 } ; :: thesis: b in proj2 f
then consider x, y being positive Nat such that
A13: b = [x,y] and
A14: x + y = m + 1 ;
A15: 0 + 1 <= x by NAT_1:13;
x + 0 < x + y by XREAL_1:6;
then x <= m by A14, NAT_1:13;
then A16: x in Seg m by A15;
then S₁[x,f . x] by A4;
then f . x = [x,((m - x) + 1)]
.= [x,y] by A14 ;
hence b in proj2 f by A3, A13, A16, FUNCT_1:def 3; :: thesis: verum

end;

A17: Seg m,m are_equipotent by FINSEQ_1:54;
card m = m ;
hence card { [x,y] where x, y is positive Nat : x + y = m + 1 } = m by A1, A17, WELLORD2:15, CARD_1:5; :: thesis: verum