let X be complex-membered set ; :: thesis: multRel (X,1) = id X

now :: thesis: for x, y being object holds
( ( [x,y] in multRel (X,1) implies ( x in X & x = y ) ) & ( x in X & x = y implies [x,y] in multRel (X,1) ) )

let x, y be object ; :: thesis: ( ( [x,y] in multRel (X,1) implies ( x in X & x = y ) ) & ( x in X & x = y implies [x,y] in multRel (X,1) ) )

hereby :: thesis: ( x in X & x = y implies [x,y] in multRel (X,1) )

assume A1: [x,y] in multRel (X,1) ; :: thesis: ( x in X & x = y )
reconsider z1 = x, z2 = y as set by TARSKI:1;
[z1,z2] in multRel (X,1) by A1;
then ( z1 in X & z2 in X ) by MMLQUER2:4;
then reconsider z1 = z1, z2 = z2 as Complex ;
[z1,z2] in multRel (X,1) by A1;
then ( z1 in X & z2 = 1 * z1 ) by Th42;
hence ( x in X & x = y ) ; :: thesis: verum

end;

assume A2: ( x in X & x = y ) ; :: thesis: [x,y] in multRel (X,1)
then reconsider z1 = x, z2 = y as Complex ;
z2 = 1 * z1 by A2;
hence [x,y] in multRel (X,1) by A2, Th42; :: thesis: verum

end;

hence multRel (X,1) = id X by RELAT_1:def 10; :: thesis: verum