let a, b, x, X, y, Y, z, Z be set ; :: thesis: for c being complex number st a,b,c are_mutually_different & 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 c be complex number ; :: thesis: ( a,b,c are_mutually_different & 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_different ; :: 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 Th32;
then {((a,b,c) --> (x,y,z))} c= product ((a,b,c) --> (X,Y,Z)) by A1, Th31;
hence (a,b,c) --> (x,y,z) in product ((a,b,c) --> (X,Y,Z)) by ZFMISC_1:31; :: thesis: verum