let p be Point of (TOP-REAL 2); :: thesis: for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f = Sq_Circ & p `1 = - 1 & p `2 < 0 holds
( (f . p) `1 < 0 & (f . p) `2 < 0 )
let f be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis: ( f = Sq_Circ & p `1 = - 1 & p `2 < 0 implies ( (f . p) `1 < 0 & (f . p) `2 < 0 ) )
assume A1: ( f = Sq_Circ & p `1 = - 1 & p `2 < 0 ) ; :: thesis: ( (f . p) `1 < 0 & (f . p) `2 < 0 )
now
per cases ( p = 0. (TOP-REAL 2) or p <> 0. (TOP-REAL 2) ) ;
case A2: p <> 0. (TOP-REAL 2) ; :: thesis: ( (f . p) `1 < 0 & (f . p) `2 < 0 )
now
per cases ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or ( not ( p `2 <= p `1 & - (p `1 ) <= p `2 ) & not ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) ) ;
case ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) ; :: thesis: ( (f . p) `1 < 0 & (f . p) `2 < 0 )
then f . p = |[((p `1 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]| by A1, A2, JGRAPH_3:def 1;
then A3: ( (f . p) `1 = (p `1 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))) & (f . p) `2 = (p `2 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))) ) by EUCLID:56;
A4: ((p `2 ) / (p `1 )) ^2 >= 0 by XREAL_1:65;
sqrt (1 + (((p `2 ) / (p `1 )) ^2 )) > 0 by A4, SQUARE_1:93;
hence ( (f . p) `1 < 0 & (f . p) `2 < 0 ) by A1, A3, XREAL_1:143; :: thesis: verum
end;
case ( not ( p `2 <= p `1 & - (p `1 ) <= p `2 ) & not ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) ; :: thesis: ( (f . p) `1 < 0 & (f . p) `2 < 0 )
then f . p = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| by A1, A2, JGRAPH_3:def 1;
then A5: ( (f . p) `1 = (p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))) & (f . p) `2 = (p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))) ) by EUCLID:56;
A6: ((p `1 ) / (p `2 )) ^2 >= 0 by XREAL_1:65;
sqrt (1 + (((p `1 ) / (p `2 )) ^2 )) > 0 by A6, SQUARE_1:93;
hence ( (f . p) `1 < 0 & (f . p) `2 < 0 ) by A1, A5, XREAL_1:143; :: thesis: verum
end;
end;
end;
hence ( (f . p) `1 < 0 & (f . p) `2 < 0 ) ; :: thesis: verum
end;
end;
end;
hence ( (f . p) `1 < 0 & (f . p) `2 < 0 ) ; :: thesis: verum