let a1, a2, a3, a4 be object ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( not a2 <> a3 or not a2 <> a4 or not a3 <> a4 or <*a1,a2,a3,a4*> is one-to-one )
assume A4: a2 <> a3 ; :: thesis: ( not a2 <> a4 or not a3 <> a4 or <*a1,a2,a3,a4*> is one-to-one )
assume A5: a2 <> a4 ; :: thesis: ( not a3 <> a4 or <*a1,a2,a3,a4*> is one-to-one )
assume A6: a3 <> a4 ; :: thesis: <*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 ; :: according to FUNCT_1:def 4 :: thesis: ( 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*> ; :: thesis: ( 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*> ; :: thesis: ( 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; :: thesis: verum