let X be set ; :: thesis: for L1, L2 being List of X

for O1, O2 being Operation of X st L1 c= L2 & O1 c= O2 holds

L1 | O1 c= L2 | O2

let L1, L2 be List of X; :: thesis: for O1, O2 being Operation of X st L1 c= L2 & O1 c= O2 holds

L1 | O1 c= L2 | O2

let O1, O2 be Operation of X; :: thesis: ( L1 c= L2 & O1 c= O2 implies L1 | O1 c= L2 | O2 )

assume ( L1 c= L2 & O1 c= O2 ) ; :: thesis: L1 | O1 c= L2 | O2

then ( L1 | O1 c= L2 | O1 & L2 | O1 c= L2 | O2 ) by RELAT_1:123, RELAT_1:124;

hence L1 | O1 c= L2 | O2 ; :: thesis: verum

for O1, O2 being Operation of X st L1 c= L2 & O1 c= O2 holds

L1 | O1 c= L2 | O2

let L1, L2 be List of X; :: thesis: for O1, O2 being Operation of X st L1 c= L2 & O1 c= O2 holds

L1 | O1 c= L2 | O2

let O1, O2 be Operation of X; :: thesis: ( L1 c= L2 & O1 c= O2 implies L1 | O1 c= L2 | O2 )

assume ( L1 c= L2 & O1 c= O2 ) ; :: thesis: L1 | O1 c= L2 | O2

then ( L1 | O1 c= L2 | O1 & L2 | O1 c= L2 | O2 ) by RELAT_1:123, RELAT_1:124;

hence L1 | O1 c= L2 | O2 ; :: thesis: verum