let N be Nat; :: thesis: for V being set
for loc being b₁ -valued Function st loc | (Seg N) is one-to-one & Seg N c= dom loc holds
for i, j being Nat st 1 <= i & i <= N & 1 <= j & j <= N & i <> j holds
loc /. i <> loc /. j
let V be set ; :: thesis: for loc being V -valued Function st loc | (Seg N) is one-to-one & Seg N c= dom loc holds
for i, j being Nat st 1 <= i & i <= N & 1 <= j & j <= N & i <> j holds
loc /. i <> loc /. j
let loc be V -valued Function; :: thesis: ( loc | (Seg N) is one-to-one & Seg N c= dom loc implies for i, j being Nat st 1 <= i & i <= N & 1 <= j & j <= N & i <> j holds
loc /. i <> loc /. j )
set f = loc | (Seg N);
assume that
A1: loc | (Seg N) is one-to-one and
A2: Seg N c= dom loc ; :: thesis: for i, j being Nat st 1 <= i & i <= N & 1 <= j & j <= N & i <> j holds
loc /. i <> loc /. j
let i, j be Nat; :: thesis: ( 1 <= i & i <= N & 1 <= j & j <= N & i <> j implies loc /. i <> loc /. j )
assume that
A3: ( 1 <= i & i <= N ) and
A4: ( 1 <= j & j <= N ) and
A5: i <> j ; :: thesis: loc /. i <> loc /. j
A6: i in Seg N by A3, FINSEQ_1:1;
then A7: i in dom (loc | (Seg N)) by A2, RELAT_1:57;
A8: j in Seg N by A4, FINSEQ_1:1;
then A9: j in dom (loc | (Seg N)) by A2, RELAT_1:57;
A10: loc /. i = loc . i by A2, A6, PARTFUN1:def 6;
A11: (loc | (Seg N)) . i = loc . i by A7, FUNCT_1:47;
(loc | (Seg N)) . j = loc . j by A9, FUNCT_1:47;
hence loc /. i <> loc /. j by A1, A5, A7, A9, A10, A2, A8, A11, FUNCT_1:def 4, PARTFUN1:def 6; :: thesis: verum