let z be Complex; :: thesis: multRel (COMPLEX,z) = { [z1,(z1 * z)] where z1 is Complex : verum }
set S = { [z1,(z1 * z)] where z1 is Complex : verum } ;

now :: thesis: for o being object holds
( ( o in multRel (COMPLEX,z) implies o in { [z1,(z1 * z)] where z1 is Complex : verum } ) & ( o in { [z1,(z1 * z)] where z1 is Complex : verum } implies o in multRel (COMPLEX,z) ) )

let o be object ; :: thesis: ( ( o in multRel (COMPLEX,z) implies o in { [z1,(z1 * z)] where z1 is Complex : verum } ) & ( o in { [z1,(z1 * z)] where z1 is Complex : verum } implies o in multRel (COMPLEX,z) ) )

hereby :: thesis: ( o in { [z1,(z1 * z)] where z1 is Complex : verum } implies o in multRel (COMPLEX,z) )

assume A1: o in multRel (COMPLEX,z) ; :: thesis: o in { [z1,(z1 * z)] where z1 is Complex : verum }
then consider x, y being object such that
A2: o = [x,y] by RELAT_1:def 1;
reconsider x = x, y = y as set by TARSKI:1;
[x,y] in multRel (COMPLEX,z) by A1, A2;
then ( x in COMPLEX & y in COMPLEX ) by MMLQUER2:4;
then reconsider x = x, y = y as Complex ;
y = z * x by A1, A2, Th42;
hence o in { [z1,(z1 * z)] where z1 is Complex : verum } by A2; :: thesis: verum

end;

assume o in { [z1,(z1 * z)] where z1 is Complex : verum } ; :: thesis: o in multRel (COMPLEX,z)
then consider z1 being Complex such that
A3: o = [z1,(z1 * z)] ;
( z1 in COMPLEX & z1 * z in COMPLEX ) by XCMPLX_0:def 2;
hence o in multRel (COMPLEX,z) by A3, Th42; :: thesis: verum

end;

hence multRel (COMPLEX,z) = { [z1,(z1 * z)] where z1 is Complex : verum } by TARSKI:2; :: thesis: verum