let v be Nat; :: thesis: LAG4SQg v is one-to-one
for n1, n2 being object st n1 in dom (LAG4SQg v) & n2 in dom (LAG4SQg v) & (LAG4SQg v) . n1 = (LAG4SQg v) . n2 holds
n1 = n2
proof
let n1, n2 be object ; :: thesis: ( n1 in dom (LAG4SQg v) & n2 in dom (LAG4SQg v) & (LAG4SQg v) . n1 = (LAG4SQg v) . n2 implies n1 = n2 )
assume that
A1: n1 in dom (LAG4SQg v) and
A2: n2 in dom (LAG4SQg v) and
A3: (LAG4SQg v) . n1 = (LAG4SQg v) . n2 ; :: thesis: n1 = n2
A4: dom (LAG4SQg v) = Seg (len (LAG4SQg v)) by FINSEQ_1:def 3
.= Seg v by Def3 ;
consider m1 being Nat such that
A5: n1 = m1 and
A6: 1 <= m1 and
m1 <= v by A1, A4;
consider m2 being Nat such that
A7: n2 = m2 and
A8: 1 <= m2 and
m2 <= v by A2, A4;
( (LAG4SQg v) . m1 = (LAG4SQg v) . m2 implies m1 = m2 )
proof
assume A11: (LAG4SQg v) . m1 = (LAG4SQg v) . m2 ; :: thesis: m1 = m2
assume A12: m1 <> m2 ; :: thesis: contradiction
A13: (LAG4SQg v) . m1 = (- 1) - ((m1 - 1) ^2) by Def3, A5, A1;
(LAG4SQg v) . m2 = (- 1) - ((m2 - 1) ^2) by Def3, A2, A7;
then A14: ((LAG4SQg v) . m1) - ((LAG4SQg v) . m2) = ((m2 + m1) - 2) * (m2 - m1) by A13;
A16: (m2 + m1) - 2 > 0
proof
per cases ( m2 = 1 or m2 > 1 ) by A8, XXREAL_0:1;
suppose m2 = 1 ; :: thesis: (m2 + m1) - 2 > 0
then A18: m1 > 1 by A6, A12, XXREAL_0:1;
A19: m1 + m2 > 1 + 1 by A8, A18, XREAL_1:8;
(m1 + m2) + (- 2) > 2 + (- 2) by A19, XREAL_1:8;
hence (m2 + m1) - 2 > 0 ; :: thesis: verum
end;
suppose m2 > 1 ; :: thesis: (m2 + m1) - 2 > 0
then A20: m1 + m2 > 1 + 1 by A6, XREAL_1:8;
(m1 + m2) + (- 2) > 2 + (- 2) by A20, XREAL_1:8;
hence (m2 + m1) - 2 > 0 ; :: thesis: verum
end;
end;
end;
m2 - m1 <> 0 by A12;
hence contradiction by A11, A14, A16; :: thesis: verum
end;
hence n1 = n2 by A5, A7, A3; :: thesis: verum
end;
hence LAG4SQg v is one-to-one by FUNCT_1:def 4; :: thesis: verum