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:19, ZFMISC_1:12;
then ( dom ([:X,Y:] --> (1. Z_2 )) = [:X,Y:] & rng ([:X,Y:] --> (1. Z_2 )) c= {(0. Z_2 ),(1. Z_2 )} ) by FUNCOP_1:19, XBOOLE_1:1;
hence [:X,Y:] --> (1. Z_2 ) is incidence-matrix of X,Y by FUNCT_2:def 2; :: thesis: verum