let S, T be non empty antisymmetric RelStr ; :: thesis: for x, y being Element of [:S,T:] holds
( ex_inf_of {x,y},[:S,T:] iff ( ex_inf_of {(x `1),(y `1)},S & ex_inf_of {(x `2),(y `2)},T ) )
let x, y be Element of [:S,T:]; :: thesis: ( ex_inf_of {x,y},[:S,T:] iff ( ex_inf_of {(x `1),(y `1)},S & ex_inf_of {(x `2),(y `2)},T ) )
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def 2;
then ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by MCART_1:21;
then ( proj1 {x,y} = {(x `1),(y `1)} & proj2 {x,y} = {(x `2),(y `2)} ) by FUNCT_5:13;
hence ( ex_inf_of {x,y},[:S,T:] iff ( ex_inf_of {(x `1),(y `1)},S & ex_inf_of {(x `2),(y `2)},T ) ) by YELLOW_3:42; :: thesis: verum