let pm be Element of REAL ; :: thesis: for k being Nat st k > 0 & pm <> 0 holds
GoCross_Seq_REAL (pm,k) is one-to-one
let k be Nat; :: thesis: ( k > 0 & pm <> 0 implies GoCross_Seq_REAL (pm,k) is one-to-one )
assume A1: ( k > 0 & pm <> 0 ) ; :: thesis: 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 ; :: thesis: ( 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)) ; :: thesis: ( 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)) ; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum

end;

hence GoCross_Seq_REAL (pm,k) is one-to-one by FUNCT_1:def 4; :: thesis: verum