let pm be Element of REAL ; for k being Nat st k > 0 & pm <> 0 holds
GoCross_Seq_REAL (pm,k) is one-to-one
let k be Nat; ( k > 0 & pm <> 0 implies GoCross_Seq_REAL (pm,k) is one-to-one )
assume A1:
( k > 0 & pm <> 0 )
; GoCross_Seq_REAL (pm,k) is one-to-one
for x1, x2 being object st x1 in dom (GoCross_Seq_REAL (pm,k)) & x2 in dom (GoCross_Seq_REAL (pm,k)) & (GoCross_Seq_REAL (pm,k)) . x1 = (GoCross_Seq_REAL (pm,k)) . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom (GoCross_Seq_REAL (pm,k)) & x2 in dom (GoCross_Seq_REAL (pm,k)) & (GoCross_Seq_REAL (pm,k)) . x1 = (GoCross_Seq_REAL (pm,k)) . x2 implies x1 = x2 )
assume B1:
x1 in dom (GoCross_Seq_REAL (pm,k))
;
( not x2 in dom (GoCross_Seq_REAL (pm,k)) or not (GoCross_Seq_REAL (pm,k)) . x1 = (GoCross_Seq_REAL (pm,k)) . x2 or x1 = x2 )
assume B2:
x2 in dom (GoCross_Seq_REAL (pm,k))
;
( not (GoCross_Seq_REAL (pm,k)) . x1 = (GoCross_Seq_REAL (pm,k)) . x2 or x1 = x2 )
assume B3:
(GoCross_Seq_REAL (pm,k)) . x1 = (GoCross_Seq_REAL (pm,k)) . x2
;
x1 = x2
reconsider x1 =
x1 as
Nat by B1;
reconsider x2 =
x2 as
Nat by B2;
set d1 =
(pm * k) * ((x1 + 1) ");
(
{((pm * k) * ((x1 + 1) "))} = (GoCross_Seq_REAL (pm,k)) . x1 &
{((pm * k) * ((x2 + 1) "))} = (GoCross_Seq_REAL (pm,k)) . x2 )
by Def4;
then B8:
(pm * k) * ((x1 + 1) ") in {((pm * k) * ((x2 + 1) "))}
by TARSKI:def 1, B3;
(pm ") * (pm * (k * ((x1 + 1) "))) = (pm ") * (pm * (k * ((x2 + 1) ")))
by TARSKI:def 1, B8;
then C1:
((pm ") * pm) * (k * ((x1 + 1) ")) = ((pm ") * pm) * (k * ((x2 + 1) "))
;
(pm ") * pm = 1
by A1, XCMPLX_0:def 7;
then
(k ") * (k * ((x1 + 1) ")) = (k ") * (k * ((x2 + 1) "))
by C1;
then C2:
((k ") * k) * ((x1 + 1) ") = ((k ") * k) * ((x2 + 1) ")
;
(k ") * k = 1
by A1, XCMPLX_0:def 7;
then
x1 + 1
= x2 + 1
by C2, XCMPLX_1:201;
hence
x1 = x2
;
verum
end;
hence
GoCross_Seq_REAL (pm,k) is one-to-one
by FUNCT_1:def 4; verum