let a, b, c, x, y, z be object ; :: thesis: for X, Y, Z being set st a,b,c are_mutually_distinct & x in X & y in Y & z in Z holds
(a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z))
let X, Y, Z be set ; :: thesis: ( a,b,c are_mutually_distinct & x in X & y in Y & z in Z implies (a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z)) )
assume A1: a,b,c are_mutually_distinct ; :: thesis: ( not x in X or not y in Y or not z in Z or (a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z)) )
assume ( x in X & y in Y & z in Z ) ; :: thesis: (a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z))
then ( {x} c= X & {y} c= Y & {z} c= Z ) by ZFMISC_1:31;
then product ((a,b,c) --> ({x},{y},{z})) c= product ((a,b,c) --> (X,Y,Z)) by Th22;
then {((a,b,c) --> (x,y,z))} c= product ((a,b,c) --> (X,Y,Z)) by A1, Th21;
hence (a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z)) by ZFMISC_1:31; :: thesis: verum