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