let X1, X2, X3, X4 be set ; :: thesis: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} implies for x being Element of [:X1,X2,X3,X4:] holds x = [(x `1),(x `2),(x `3),(x `4)] )
assume A1: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} ) ; :: thesis: for x being Element of [:X1,X2,X3,X4:] holds x = [(x `1),(x `2),(x `3),(x `4)]
let x be Element of [:X1,X2,X3,X4:]; :: thesis: x = [(x `1),(x `2),(x `3),(x `4)]
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that
A2: x = [xx1,xx2,xx3,xx4] by A1, Lm3;
thus x = [(x `1),xx2,xx3,xx4] by A1, A2, Def8
.= [(x `1),(x `2),xx3,xx4] by A1, A2, Def9
.= [(x `1),(x `2),(x `3),xx4] by A1, A2, Def10
.= [(x `1),(x `2),(x `3),(x `4)] by A1, A2, Def11 ; :: thesis: verum