let X be set ; :: thesis: for R, S being Relation of X holds R * S = { [x,y] where x, y is Element of X : ex z being Element of X st
( [x,z] in R & [z,y] in S ) }
let R, S be Relation of X; :: thesis: R * S = { [x,y] where x, y is Element of X : ex z being Element of X st
( [x,z] in R & [z,y] in S ) }
reconsider RS = R * S as Relation of X ;
A1: R * S c= { [x,y] where x, y is Element of X : ex z being Element of X st
( [x,z] in R & [z,y] in S ) }

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in R * S or t in { [x,y] where x, y is Element of X : ex z being Element of X st
( [x,z] in R & [z,y] in S ) } )
assume A1: t in R * S ; :: thesis: t in { [x,y] where x, y is Element of X : ex z being Element of X st
( [x,z] in R & [z,y] in S ) }
consider x1, x2 being object such that
x1 in X and
A2: x2 in X and
A3: t = [x1,x2] by A1, ZFMISC_1:def 2;
consider z being object such that
A4: [x1,z] in R and
A5: [z,x2] in S by A1, A3, RELAT_1:def 8;
reconsider x1 = x1, x2 = x2, z1 = z as Element of X by A2, A4, ZFMISC_1:87;
( [x1,z1] in R & [z1,x2] in S ) by A4, A5;
hence t in { [x,y] where x, y is Element of X : ex z being Element of X st
( [x,z] in R & [z,y] in S ) } by A3; :: thesis: verum

end;

{ [x,y] where x, y is Element of X : ex z being Element of X st
( [x,z] in R & [z,y] in S ) } c= R * S

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { [x,y] where x, y is Element of X : ex z being Element of X st
( [x,z] in R & [z,y] in S ) } or t in R * S )
assume t in { [x,y] where x, y is Element of X : ex z being Element of X st
( [x,z] in R & [z,y] in S ) } ; :: thesis: t in R * S
then ex x, y being Element of X st
( t = [x,y] & ex z being Element of X st
( [x,z] in R & [z,y] in S ) ) ;
hence t in R * S by RELAT_1:def 8; :: thesis: verum

end;

hence R * S = { [x,y] where x, y is Element of X : ex z being Element of X st
( [x,z] in R & [z,y] in S ) } by A1; :: thesis: verum