let D be non empty set ; :: thesis: for g being FinSequence of D holds
( g is one-to-one iff for i1, i2 being 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 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: ( ( for i1, i2 being 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 A2: for i1, i2 being 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 object st x1 in dom g & x2 in dom g & g . x1 = g . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 implies x1 = x2 )
assume that
A3: x1 in dom g and
A4: x2 in dom g and
A5: g . x1 = g . x2 ; :: thesis: x1 = x2
reconsider n2 = x2 as Nat by A4;
A6: 1 <= n2 by A4, FINSEQ_3:25;
reconsider n1 = x1 as Nat by A3;
A7: n1 <= len g by A3, FINSEQ_3:25;
A8: n2 <= len g by A4, FINSEQ_3:25;
1 <= n1 by A3, FINSEQ_3:25;
hence x1 = x2 by A2, A5, A7, A6, A8; :: thesis: verum

end;

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

end;

( g is one-to-one implies for i1, i2 being 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 A9: g is one-to-one ; :: thesis: for i1, i2 being 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 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 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 that
A10: 1 <= i1 and
A11: i1 <= len g and
A12: 1 <= i2 and
A13: i2 <= len g and
A14: ( g . i1 = g . i2 or g /. i1 = g /. i2 ) ; :: thesis: i1 = i2
A15: i2 in dom g by A12, A13, FINSEQ_3:25;
A16: g /. i2 = g . i2 by A12, A13, FINSEQ_4:15;
A17: g /. i1 = g . i1 by A10, A11, FINSEQ_4:15;
i1 in dom g by A10, A11, FINSEQ_3:25;
hence i1 = i2 by A9, A14, A15, A17, A16, FUNCT_1:def 4; :: thesis: verum

end;

end;

hence ( g is one-to-one iff for i1, i2 being 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