let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in K51((f /^ 1)) or not x2 in K51((f /^ 1)) or not (f /^ 1) . x1 = (f /^ 1) . x2 or x1 = x2 )
assume that
A1: x1 in dom (f /^ 1) and
A2: x2 in dom (f /^ 1) and
A3: (f /^ 1) . x1 = (f /^ 1) . x2 ; :: thesis: x1 = x2
reconsider i = x1, j = x2 as Nat by A1, A2;
1 <= i by A1, FINSEQ_3:25;
then A4: 1 < i + 1 by NAT_1:13;
i + 1 in dom f by A1, FINSEQ_5:26;
then A5: i + 1 <= len f by FINSEQ_3:25;
1 <= j by A2, FINSEQ_3:25;
then A6: 1 < j + 1 by NAT_1:13;
j + 1 in dom f by A2, FINSEQ_5:26;
then A7: j + 1 <= len f by FINSEQ_3:25;
assume A8: x1 <> x2 ; :: thesis: contradiction
per cases ( i < j or j < i ) by A8, XXREAL_0:1;
suppose i < j ; :: thesis: contradiction
then A9: i + 1 < j + 1 by XREAL_1:6;
f /. (i + 1) = (f /^ 1) /. i by A1, FINSEQ_5:27
.= (f /^ 1) . j by A1, A3, PARTFUN1:def 6
.= (f /^ 1) /. j by A2, PARTFUN1:def 6
.= f /. (j + 1) by A2, FINSEQ_5:27 ;
hence contradiction by A4, A7, A9, GOBOARD7:37; :: thesis: verum
end;
suppose j < i ; :: thesis: contradiction
then A10: j + 1 < i + 1 by XREAL_1:6;
f /. (j + 1) = (f /^ 1) /. j by A2, FINSEQ_5:27
.= (f /^ 1) . i by A2, A3, PARTFUN1:def 6
.= (f /^ 1) /. i by A1, PARTFUN1:def 6
.= f /. (i + 1) by A1, FINSEQ_5:27 ;
hence contradiction by A5, A6, A10, GOBOARD7:37; :: thesis: verum
end;
end;