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