let D be non empty set ; 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; ( 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 )
( 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
;
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
verumproof
let i1,
i2 be
Nat;
( 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 )
;
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;
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; verum