let a1, a2, a3, a4 be object ; ( a1 <> a2 & a1 <> a3 & a1 <> a4 & a2 <> a3 & a2 <> a4 & a3 <> a4 implies <*a1,a2,a3,a4*> is one-to-one )
assume A1:
a1 <> a2
; ( not a1 <> a3 or not a1 <> a4 or not a2 <> a3 or not a2 <> a4 or not a3 <> a4 or <*a1,a2,a3,a4*> is one-to-one )
assume A2:
a1 <> a3
; ( not a1 <> a4 or not a2 <> a3 or not a2 <> a4 or not a3 <> a4 or <*a1,a2,a3,a4*> is one-to-one )
assume A3:
a1 <> a4
; ( not a2 <> a3 or not a2 <> a4 or not a3 <> a4 or <*a1,a2,a3,a4*> is one-to-one )
assume A4:
a2 <> a3
; ( not a2 <> a4 or not a3 <> a4 or <*a1,a2,a3,a4*> is one-to-one )
assume A5:
a2 <> a4
; ( not a3 <> a4 or <*a1,a2,a3,a4*> is one-to-one )
assume A6:
a3 <> a4
; <*a1,a2,a3,a4*> is one-to-one
A7:
dom <*a1,a2,a3,a4*> = Seg 4
by FINSEQ_1:89;
let x, y be object ; FUNCT_1:def 4 ( not x in proj1 <*a1,a2,a3,a4*> or not y in proj1 <*a1,a2,a3,a4*> or not <*a1,a2,a3,a4*> . x = <*a1,a2,a3,a4*> . y or x = y )
assume
x in dom <*a1,a2,a3,a4*>
; ( not y in proj1 <*a1,a2,a3,a4*> or not <*a1,a2,a3,a4*> . x = <*a1,a2,a3,a4*> . y or x = y )
then A8:
( x = 1 or x = 2 or x = 3 or x = 4 )
by A7, ENUMSET1:def 2, FINSEQ_3:2;
assume A9:
y in dom <*a1,a2,a3,a4*>
; ( not <*a1,a2,a3,a4*> . x = <*a1,a2,a3,a4*> . y or x = y )
( <*a1,a2,a3,a4*> . 1 = a1 & <*a1,a2,a3,a4*> . 2 = a2 & <*a1,a2,a3,a4*> . 3 = a3 & <*a1,a2,a3,a4*> . 4 = a4 )
by FINSEQ_4:76;
hence
( not <*a1,a2,a3,a4*> . x = <*a1,a2,a3,a4*> . y or x = y )
by A1, A2, A3, A4, A5, A6, A8, A7, A9, ENUMSET1:def 2, FINSEQ_3:2; verum