let S, T be antisymmetric with_suprema RelStr ; :: thesis: for x1, y1 being Element of S
for x2, y2 being Element of T holds [(x1 "\/" y1),(x2 "\/" y2)] = [x1,x2] "\/" [y1,y2]
let x1, y1 be Element of S; :: thesis: for x2, y2 being Element of T holds [(x1 "\/" y1),(x2 "\/" y2)] = [x1,x2] "\/" [y1,y2]
let x2, y2 be Element of T; :: thesis: [(x1 "\/" y1),(x2 "\/" y2)] = [x1,x2] "\/" [y1,y2]
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2;
A2: ([x1,x2] "\/" [y1,y2]) `2 = ([x1,x2] `2 ) "\/" ([y1,y2] `2 ) by Th14
.= x2 "\/" ([y1,y2] `2 ) by MCART_1:7
.= x2 "\/" y2 by MCART_1:7
.= [(x1 "\/" y1),(x2 "\/" y2)] `2 by MCART_1:7 ;
([x1,x2] "\/" [y1,y2]) `1 = ([x1,x2] `1 ) "\/" ([y1,y2] `1 ) by Th14
.= x1 "\/" ([y1,y2] `1 ) by MCART_1:7
.= x1 "\/" y1 by MCART_1:7
.= [(x1 "\/" y1),(x2 "\/" y2)] `1 by MCART_1:7 ;
hence [(x1 "\/" y1),(x2 "\/" y2)] = [x1,x2] "\/" [y1,y2] by A1, A2, DOMAIN_1:12; :: thesis: verum