let X1, X2, X3, X4, X5, X6, X7 be set ; ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} implies for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] holds x = [(x `1),(x `2),(x `3),(x `4),(x `5),(x `6),(x `7)] )
assume A1:
( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} )
; for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] holds x = [(x `1),(x `2),(x `3),(x `4),(x `5),(x `6),(x `7)]
let x be Element of [:X1,X2,X3,X4,X5,X6,X7:]; x = [(x `1),(x `2),(x `3),(x `4),(x `5),(x `6),(x `7)]
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, xx6 being Element of X6, xx7 being Element of X7 such that
A2:
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7]
by A1, Th94;
thus x =
[(x `1),xx2,xx3,xx4,xx5,xx6,xx7]
by A1, A2, Def18
.=
[(x `1),(x `2),xx3,xx4,xx5,xx6,xx7]
by A1, A2, Def19
.=
[(x `1),(x `2),(x `3),xx4,xx5,xx6,xx7]
by A1, A2, Def20
.=
[(x `1),(x `2),(x `3),(x `4),xx5,xx6,xx7]
by A1, A2, Def21
.=
[(x `1),(x `2),(x `3),(x `4),(x `5),xx6,xx7]
by A1, A2, Def22
.=
[(x `1),(x `2),(x `3),(x `4),(x `5),(x `6),xx7]
by A1, A2, Def23
.=
[(x `1),(x `2),(x `3),(x `4),(x `5),(x `6),(x `7)]
by A1, A2, Def24
; verum