let n be Nat; :: thesis: n block n = 1
set F = { f where f is Function of (Segm n),(Segm n) : ( f is onto & f is "increasing ) } ;
A1: { f where f is Function of (Segm n),(Segm n) : ( f is onto & f is "increasing ) } c= {(id n)}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (Segm n),(Segm n) : ( f is onto & f is "increasing ) } or x in {(id n)} )
assume x in { f where f is Function of (Segm n),(Segm n) : ( f is onto & f is "increasing ) } ; :: thesis: x in {(id n)}
then consider f being Function of (Segm n),(Segm n) such that
A2: x = f and
A3: ( f is onto & f is "increasing ) ;
f = id n by ;
hence x in {(id n)} by ; :: thesis: verum
end;
( n = 0 iff n = 0 ) ;
then consider f being Function of (Segm n),(Segm n) such that
A4: ( f is onto & f is "increasing ) by Th23;
f in { f where f is Function of (Segm n),(Segm n) : ( f is onto & f is "increasing ) } by A4;
then { f where f is Function of (Segm n),(Segm n) : ( f is onto & f is "increasing ) } = {(id n)} by ;
hence n block n = 1 by CARD_1:30; :: thesis: verum