let n be Nat; :: thesis: sqr (cot (x_r-seq n)) is one-to-one
set f = x_r-seq n;
A1: x_r-seq n is one-to-one by Th25;
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (sqr (cot (x_r-seq n))) or not x2 in dom (sqr (cot (x_r-seq n))) or not (sqr (cot (x_r-seq n))) . x1 = (sqr (cot (x_r-seq n))) . x2 or x1 = x2 )
assume A2: ( x1 in dom (sqr (cot (x_r-seq n))) & x2 in dom (sqr (cot (x_r-seq n))) & (sqr (cot (x_r-seq n))) . x1 = (sqr (cot (x_r-seq n))) . x2 ) ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Nat by A2;
A3: ( len (sqr (cot (x_r-seq n))) = len (cot (x_r-seq n)) & len (cot (x_r-seq n)) = len (x_r-seq n) & len (x_r-seq n) = n ) by CARD_1:def 7;
then A4: ( dom (sqr (cot (x_r-seq n))) = dom (cot (x_r-seq n)) & dom (cot (x_r-seq n)) = dom (x_r-seq n) ) by FINSEQ_3:29;
( 1 <= x1 & x1 <= n & 1 <= x2 & x2 <= n ) by FINSEQ_3:25, A3, A2;
then A5: ( 0 < (x_r-seq n) . x1 & (x_r-seq n) . x1 < PI / 2 & 0 < (x_r-seq n) . x2 & (x_r-seq n) . x2 < PI / 2 & PI / 2 < PI ) by Th21, COMPTRIG:5;
then ( (x_r-seq n) . x1 < PI & (x_r-seq n) . x2 < PI ) by XXREAL_0:2;
then A6: ( (x_r-seq n) . x1 in ].0,PI.[ & (x_r-seq n) . x2 in ].0,PI.[ & (x_r-seq n) . x1 in ].0,(PI / 2).[ & (x_r-seq n) . x2 in ].0,(PI / 2).[ ) by A5, XXREAL_1:4;
then A7: ( sin ((x_r-seq n) . x1) > 0 & sin ((x_r-seq n) . x2) > 0 & cos ((x_r-seq n) . x1) > 0 & cos ((x_r-seq n) . x2) > 0 ) by COMPTRIG:7, SIN_COS:80;
A8: ( (cot (x_r-seq n)) . x1 = cot ((x_r-seq n) . x1) & (cot (x_r-seq n)) . x2 = cot ((x_r-seq n) . x2) ) by Def3, A2, A4;
A9: cot ((x_r-seq n) . x1) = cot ((x_r-seq n) . x2)
proof
( (sqr (cot (x_r-seq n))) . x1 = ((cot (x_r-seq n)) . x1) ^2 & (sqr (cot (x_r-seq n))) . x2 = ((cot (x_r-seq n)) . x2) ^2 ) by VALUED_1:11;
then ( (cot (x_r-seq n)) . x1 = (cot (x_r-seq n)) . x2 or (cot (x_r-seq n)) . x1 = - ((cot (x_r-seq n)) . x2) ) by A2, SQUARE_1:40;
hence cot ((x_r-seq n) . x1) = cot ((x_r-seq n) . x2) by A7, A8; :: thesis: verum
end;
(x_r-seq n) . x1 = (x_r-seq n) . x2
proof
A10: ( cot . ((x_r-seq n) . x1) = cot ((x_r-seq n) . x1) & cot . ((x_r-seq n) . x2) = cot ((x_r-seq n) . x2) ) by A6, SIN_COS9:2, RFUNCT_1:def 1;
A11: ( (x_r-seq n) . x1 in dom (cot | ].0,PI.[) & (x_r-seq n) . x2 in dom (cot | ].0,PI.[) ) by A6, SIN_COS9:2, RELAT_1:57;
then ( cot . ((x_r-seq n) . x1) = (cot | ].0,PI.[) . ((x_r-seq n) . x1) & cot . ((x_r-seq n) . x2) = (cot | ].0,PI.[) . ((x_r-seq n) . x2) ) by FUNCT_1:47;
hence (x_r-seq n) . x1 = (x_r-seq n) . x2 by A9, A10, A11, FUNCT_1:def 4, SIN_COS9:10; :: thesis: verum
end;
hence x1 = x2 by A1, A2, A4, FUNCT_1:def 4; :: thesis: verum