let x be Element of [:S,T:]; :: according to WAYBEL_1:def 24 :: thesis: ex b₁ being M2(the carrier of [:S,T:]) st b₁ is_a_complement_of x
consider s being Element of S such that
A1: s is_a_complement_of x `1 by WAYBEL_1:def 24;
consider t being Element of T such that
A2: t is_a_complement_of x `2 by WAYBEL_1:def 24;
take [s,t] ; :: thesis: [s,t] is_a_complement_of x
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2;
then ( [s,t] `1 = s & [s,t] `2 = t & x = [(x `1 ),(x `2 )] ) by MCART_1:7, MCART_1:23;
hence [s,t] is_a_complement_of x by A1, A2, Th17; :: thesis: verum