let X, Y be set ; :: thesis: [:X,Y:] --> (1. Z_2) is incidence-matrix of X,Y
set f = [:X,Y:] --> (1. Z_2);
( rng ([:X,Y:] --> (1. Z_2)) c= {(1. Z_2)} & {(1. Z_2)} c= {(0. Z_2),(1. Z_2)} ) by FUNCOP_1:13, ZFMISC_1:7;
then ( dom ([:X,Y:] --> (1. Z_2)) = [:X,Y:] & rng ([:X,Y:] --> (1. Z_2)) c= {(0. Z_2),(1. Z_2)} ) ;
hence [:X,Y:] --> (1. Z_2) is incidence-matrix of X,Y by FUNCT_2:def 2; :: thesis: verum