for X, Y being set st X <> {} & Y <> {} holds
for x being Element of [:X,Y:] holds x = [(x `1),(x `2)] by Th15;