let X, Y, Z, x, y be set ; :: thesis: for f being Function of [:X,Y:],Z st x in X & y in Y & Z <> {} holds
f . x,y in Z
let f be Function of [:X,Y:],Z; :: thesis: ( x in X & y in Y & Z <> {} implies f . x,y in Z )
assume ( x in X & y in Y ) ; :: thesis: ( not Z <> {} or f . x,y in Z )
then [x,y] in [:X,Y:] by ZFMISC_1:106;
hence ( not Z <> {} or f . x,y in Z ) by FUNCT_2:7; :: thesis: verum