let D be non empty set ; :: thesis: for g being FinSequence of D holds
( g is one-to-one iff for i1, i2 being Element of NAT st 1 <= i1 & i1 <= len g & 1 <= i2 & i2 <= len g & ( g . i1 = g . i2 or g /. i1 = g /. i2 ) holds
i1 = i2 )
let g be FinSequence of D; :: thesis: ( g is one-to-one iff for i1, i2 being Element of NAT st 1 <= i1 & i1 <= len g & 1 <= i2 & i2 <= len g & ( g . i1 = g . i2 or g /. i1 = g /. i2 ) holds
i1 = i2 )
A1: ( g is one-to-one implies for i1, i2 being Element of NAT st 1 <= i1 & i1 <= len g & 1 <= i2 & i2 <= len g & ( g . i1 = g . i2 or g /. i1 = g /. i2 ) holds
i1 = i2 )

proof

assume A2: g is one-to-one ; :: thesis: for i1, i2 being Element of NAT st 1 <= i1 & i1 <= len g & 1 <= i2 & i2 <= len g & ( g . i1 = g . i2 or g /. i1 = g /. i2 ) holds
i1 = i2
thus for i1, i2 being Element of NAT st 1 <= i1 & i1 <= len g & 1 <= i2 & i2 <= len g & ( g . i1 = g . i2 or g /. i1 = g /. i2 ) holds
i1 = i2 :: thesis: verum

proof

let i1, i2 be Element of NAT ; :: thesis: ( 1 <= i1 & i1 <= len g & 1 <= i2 & i2 <= len g & ( g . i1 = g . i2 or g /. i1 = g /. i2 ) implies i1 = i2 )
assume A3: ( 1 <= i1 & i1 <= len g & 1 <= i2 & i2 <= len g & ( g . i1 = g . i2 or g /. i1 = g /. i2 ) ) ; :: thesis: i1 = i2
then A4: i1 in dom g by FINSEQ_3:27;
A5: i2 in dom g by A3, FINSEQ_3:27;
A6: g /. i1 = g . i1 by A3, FINSEQ_4:24;
g /. i2 = g . i2 by A3, FINSEQ_4:24;
hence i1 = i2 by A2, A3, A4, A5, A6, FUNCT_1:def 8; :: thesis: verum

end;

end;

( ( for i1, i2 being Element of NAT st 1 <= i1 & i1 <= len g & 1 <= i2 & i2 <= len g & ( g . i1 = g . i2 or g /. i1 = g /. i2 ) holds
i1 = i2 ) implies g is one-to-one )

proof

assume A7: for i1, i2 being Element of NAT st 1 <= i1 & i1 <= len g & 1 <= i2 & i2 <= len g & ( g . i1 = g . i2 or g /. i1 = g /. i2 ) holds
i1 = i2 ; :: thesis: g is one-to-one
for x1, x2 being set st x1 in dom g & x2 in dom g & g . x1 = g . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 implies x1 = x2 )
assume A8: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 ) ; :: thesis: x1 = x2
then reconsider n1 = x1 as Element of NAT ;
reconsider n2 = x2 as Element of NAT by A8;
A9: ( 1 <= n1 & n1 <= len g ) by A8, FINSEQ_3:27;
( 1 <= n2 & n2 <= len g ) by A8, FINSEQ_3:27;
hence x1 = x2 by A7, A8, A9; :: thesis: verum

end;

hence g is one-to-one by FUNCT_1:def 8; :: thesis: verum

end;

hence ( g is one-to-one iff for i1, i2 being Element of NAT st 1 <= i1 & i1 <= len g & 1 <= i2 & i2 <= len g & ( g . i1 = g . i2 or g /. i1 = g /. i2 ) holds
i1 = i2 ) by A1; :: thesis: verum