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