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