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:23;
then ( proj1 {x,y} = {(x `1 ),(y `1 )} & proj2 {x,y} = {(x `2 ),(y `2 )} ) by FUNCT_5:16;
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