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

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