let X, Y, Z be set ; :: thesis: for x, y being object
for f being Function of [:X,Y:],Z st x in X & y in Y & Z <> {} holds
f . (x,y) in Z
let x, y be object ; :: 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:87;
hence ( not Z <> {} or f . (x,y) in Z ) by FUNCT_2:5; :: thesis: verum