let v be Nat; :: thesis: LAG4SQf v is one-to-one
set f = LAG4SQf v;
for n1, n2 being object st n1 in dom (LAG4SQf v) & n2 in dom (LAG4SQf v) & (LAG4SQf v) . n1 = (LAG4SQf v) . n2 holds
n1 = n2

proof

let n1, n2 be object ; :: thesis: ( n1 in dom (LAG4SQf v) & n2 in dom (LAG4SQf v) & (LAG4SQf v) . n1 = (LAG4SQf v) . n2 implies n1 = n2 )
assume that
A1: n1 in dom (LAG4SQf v) and
A2: n2 in dom (LAG4SQf v) and
A3: (LAG4SQf v) . n1 = (LAG4SQf v) . n2 ; :: thesis: n1 = n2
A4: dom (LAG4SQf v) = Seg (len (LAG4SQf v)) by FINSEQ_1:def 3
.= Seg v by Def2 ;
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;
( (LAG4SQf v) . m1 = (LAG4SQf v) . m2 implies m1 = m2 )

proof

assume A11: (LAG4SQf v) . m1 = (LAG4SQf v) . m2 ; :: thesis: m1 = m2
assume A12: m1 <> m2 ; :: thesis: contradiction
A13: (LAG4SQf v) . m1 = (m1 - 1) ^2 by Def2, A5, A1;
A14: ((LAG4SQf v) . m1) - ((LAG4SQf v) . m2) = ((m1 - 1) ^2) - ((m2 - 1) ^2) by A13, Def2, A2, A7
.= ((m2 + m1) - 2) * (m1 - m2) ;
A16: (m1 + m2) - 2 > 0

proof

per cases ( m2 = 1 or m2 > 1 ) by A8, XXREAL_0:1;

suppose m2 = 1 ; :: thesis: (m1 + m2) - 2 > 0

then m1 > 1 by A12, A6, XXREAL_0:1;
then A17: m1 + m2 > 1 + 1 by A8, XREAL_1:8;
(m1 + m2) + (- 2) > 2 + (- 2) by A17, XREAL_1:8;
hence (m1 + m2) - 2 > 0 ; :: thesis: verum

end;

suppose m2 > 1 ; :: thesis: (m1 + m2) - 2 > 0

then A19: m1 + m2 > 1 + 1 by A6, XREAL_1:8;
(m1 + m2) + (- 2) > 2 + (- 2) by A19, XREAL_1:8;
hence (m1 + m2) - 2 > 0 ; :: thesis: verum

end;

end;

end;

m1 - m2 <> 0 by A12;
hence contradiction by A11, A16, A14; :: thesis: verum

end;

hence n1 = n2 by A3, A5, A7; :: thesis: verum

end;

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