let X, Y be set ; :: thesis: ( X <> {} & Y <> {} implies for x being Element of [:X,Y:] holds x = [(x `1 ),(x `2 )] )
assume ( X <> {} & Y <> {} ) ; :: thesis: for x being Element of [:X,Y:] holds x = [(x `1 ),(x `2 )]
then A1: [:X,Y:] <> {} by ZFMISC_1:113;
let x be Element of [:X,Y:]; :: thesis: x = [(x `1 ),(x `2 )]
thus x = [(x `1 ),(x `2 )] by A1, Th23; :: thesis: verum