let D, E, F be non empty set ; for P being Relation of D,E
for R being Relation of E,F
for x, z being object holds
( [x,z] in P * R iff ex y being Element of E st
( [x,y] in P & [y,z] in R ) )
let P be Relation of D,E; for R being Relation of E,F
for x, z being object holds
( [x,z] in P * R iff ex y being Element of E st
( [x,y] in P & [y,z] in R ) )
let R be Relation of E,F; for x, z being object holds
( [x,z] in P * R iff ex y being Element of E st
( [x,y] in P & [y,z] in R ) )
let x, z be object ; ( [x,z] in P * R iff ex y being Element of E st
( [x,y] in P & [y,z] in R ) )
thus
( [x,z] in P * R implies ex y being Element of E st
( [x,y] in P & [y,z] in R ) )
( ex y being Element of E st
( [x,y] in P & [y,z] in R ) implies [x,z] in P * R )proof
assume
[x,z] in P * R
;
ex y being Element of E st
( [x,y] in P & [y,z] in R )
then consider y being
object such that A1:
[x,y] in P
and A2:
[y,z] in R
by RELAT_1:def 8;
reconsider a =
y as
Element of
E by A1, ZFMISC_1:87;
take
a
;
( [x,a] in P & [a,z] in R )
thus
(
[x,a] in P &
[a,z] in R )
by A1, A2;
verum
end;
given y being Element of E such that A3:
( [x,y] in P & [y,z] in R )
; [x,z] in P * R
thus
[x,z] in P * R
by A3, RELAT_1:def 8; verum