let X1, X2, X3, X4, X5, X6, X7, X8, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8 be set ; ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & Y1 <> {} & Y2 <> {} & Y3 <> {} & Y4 <> {} & Y5 <> {} & Y6 <> {} & Y7 <> {} & Y8 <> {} implies for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]
for y being Element of [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] st x = y holds
( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 & x `5 = y `5 & x `6 = y `6 & x `7 = y `7 & x `8 = y `8 ) )
assume that
A1:
( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} )
and
A2:
( Y1 <> {} & Y2 <> {} & Y3 <> {} & Y4 <> {} & Y5 <> {} & Y6 <> {} & Y7 <> {} & Y8 <> {} )
; for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]
for y being Element of [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] st x = y holds
( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 & x `5 = y `5 & x `6 = y `6 & x `7 = y `7 & x `8 = y `8 )
let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]; for y being Element of [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] st x = y holds
( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 & x `5 = y `5 & x `6 = y `6 & x `7 = y `7 & x `8 = y `8 )
let y be Element of [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:]; ( x = y implies ( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 & x `5 = y `5 & x `6 = y `6 & x `7 = y `7 & x `8 = y `8 ) )
assume A3:
x = y
; ( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 & x `5 = y `5 & x `6 = y `6 & x `7 = y `7 & x `8 = y `8 )
thus x `1 =
((((((x `1) `1) `1) `1) `1) `1) `1
by A1, Th139
.=
y `1
by A2, A3, Th139
; ( x `2 = y `2 & x `3 = y `3 & x `4 = y `4 & x `5 = y `5 & x `6 = y `6 & x `7 = y `7 & x `8 = y `8 )
thus x `2 =
((((((x `1) `1) `1) `1) `1) `1) `2
by A1, Th139
.=
y `2
by A2, A3, Th139
; ( x `3 = y `3 & x `4 = y `4 & x `5 = y `5 & x `6 = y `6 & x `7 = y `7 & x `8 = y `8 )
thus x `3 =
(((((x `1) `1) `1) `1) `1) `2
by A1, Th139
.=
y `3
by A2, A3, Th139
; ( x `4 = y `4 & x `5 = y `5 & x `6 = y `6 & x `7 = y `7 & x `8 = y `8 )
thus x `4 =
((((x `1) `1) `1) `1) `2
by A1, Th139
.=
y `4
by A2, A3, Th139
; ( x `5 = y `5 & x `6 = y `6 & x `7 = y `7 & x `8 = y `8 )
thus x `5 =
(((x `1) `1) `1) `2
by A1, Th139
.=
y `5
by A2, A3, Th139
; ( x `6 = y `6 & x `7 = y `7 & x `8 = y `8 )
thus x `6 =
((x `1) `1) `2
by A1, Th139
.=
y `6
by A2, A3, Th139
; ( x `7 = y `7 & x `8 = y `8 )
thus x `7 =
(x `1) `2
by A1, Th139
.=
y `7
by A2, A3, Th139
; x `8 = y `8
thus x `8 =
x `2
by A1, Th139
.=
y `8
by A2, A3, Th139
; verum