let X1, X2, X3, X4, X5 be set ; :: thesis: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} implies for x being Element of [:X1,X2,X3,X4,X5:] holds x = [(x `1 ),(x `2 ),(x `3 ),(x `4 ),(x `5 )] )
assume A1: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} ) ; :: thesis: for x being Element of [:X1,X2,X3,X4,X5:] holds x = [(x `1 ),(x `2 ),(x `3 ),(x `4 ),(x `5 )]
let x be Element of [:X1,X2,X3,X4,X5:]; :: thesis: x = [(x `1 ),(x `2 ),(x `3 ),(x `4 ),(x `5 )]
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4, xx5 being Element of X5 such that
A2: x = [xx1,xx2,xx3,xx4,xx5] by A1, TH17;
thus x = [(x `1 ),xx2,xx3,xx4,xx5] by A1, A2, Def3
.= [(x `1 ),(x `2 ),xx3,xx4,xx5] by A1, A2, Def4
.= [(x `1 ),(x `2 ),(x `3 ),xx4,xx5] by A1, A2, Def5
.= [(x `1 ),(x `2 ),(x `3 ),(x `4 ),xx5] by A1, A2, Def6
.= [(x `1 ),(x `2 ),(x `3 ),(x `4 ),(x `5 )] by A1, A2, Def7 ; :: thesis: verum