theorem Th10: :: LAPLACE:10

for n, i, j being Nat st i in Seg (n + 1) & n >= 2 holds
ex Proj being Function of (2Set (Seg n)),(2Set (Seg (n + 1))) st
( rng Proj = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & Proj is one-to-one & ( for k, m being Nat st k < m & {k,m} in 2Set (Seg n) holds
( ( m < i & k < i implies Proj . {k,m} = {k,m} ) & ( m >= i & k < i implies Proj . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies Proj . {k,m} = {(k + 1),(m + 1)} ) ) ) )