let X be complex-membered set ; :: thesis: ( 0 in X implies multRel (X,0) = [:X,{0}:] )
assume A0: 0 in X ; :: thesis: multRel (X,0) = [:X,{0}:]
set M = [:X,{0}:];

now :: thesis: for x, y being object holds
( ( [x,y] in multRel (X,0) implies [x,y] in [:X,{0}:] ) & ( [x,y] in [:X,{0}:] implies [x,y] in multRel (X,0) ) )

let x, y be object ; :: thesis: ( ( [x,y] in multRel (X,0) implies [x,y] in [:X,{0}:] ) & ( [x,y] in [:X,{0}:] implies [x,y] in multRel (X,0) ) )
reconsider a = x, b = y as set by TARSKI:1;

hereby :: thesis: ( [x,y] in [:X,{0}:] implies [x,y] in multRel (X,0) )

assume A1: [x,y] in multRel (X,0) ; :: thesis: [x,y] in [:X,{0}:]
then [a,b] in multRel (X,0) ;
then ( a in X & b in X ) by MMLQUER2:4;
then reconsider a = a, b = b as Complex ;
[a,b] in multRel (X,0) by A1;
then ( a in X & b in X & b = 0 * a ) by Th42;
hence [x,y] in [:X,{0}:] by ZFMISC_1:106; :: thesis: verum

end;

assume [x,y] in [:X,{0}:] ; :: thesis: [x,y] in multRel (X,0)
then A2: ( x in X & y = 0 ) by ZFMISC_1:106;
then reconsider a = a, b = b as Complex ;
b = 0 * a by A2;
hence [x,y] in multRel (X,0) by A0, A2, Th42; :: thesis: verum

end;

hence multRel (X,0) = [:X,{0}:] by RELAT_1:def 2; :: thesis: verum