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:90;
hence x = [(x `1),(x `2)] by Th23; :: thesis: verum