let X, Y, Z, T be set ; :: thesis: for x, y, z being object

for f being Function of [:X,Y,Z:],T st x in X & y in Y & z in Z & T <> {} holds

f . (x,y,z) in T

let x, y, z be object ; :: thesis: for f being Function of [:X,Y,Z:],T st x in X & y in Y & z in Z & T <> {} holds

f . (x,y,z) in T

let f be Function of [:X,Y,Z:],T; :: thesis: ( x in X & y in Y & z in Z & T <> {} implies f . (x,y,z) in T )

assume ( x in X & y in Y & z in Z ) ; :: thesis: ( not T <> {} or f . (x,y,z) in T )

then [x,y,z] in [:X,Y,Z:] by MCART_1:69;

hence ( not T <> {} or f . (x,y,z) in T ) by FUNCT_2:5; :: thesis: verum

for f being Function of [:X,Y,Z:],T st x in X & y in Y & z in Z & T <> {} holds

f . (x,y,z) in T

let x, y, z be object ; :: thesis: for f being Function of [:X,Y,Z:],T st x in X & y in Y & z in Z & T <> {} holds

f . (x,y,z) in T

let f be Function of [:X,Y,Z:],T; :: thesis: ( x in X & y in Y & z in Z & T <> {} implies f . (x,y,z) in T )

assume ( x in X & y in Y & z in Z ) ; :: thesis: ( not T <> {} or f . (x,y,z) in T )

then [x,y,z] in [:X,Y,Z:] by MCART_1:69;

hence ( not T <> {} or f . (x,y,z) in T ) by FUNCT_2:5; :: thesis: verum