let p be Point of (); :: thesis: for P being non empty compact Subset of ()
for f being Function of (),() st f = Sq_Circ holds
( (f . p) `2 >= 0 iff p `2 >= 0 )

let P be non empty compact Subset of (); :: thesis: for f being Function of (),() st f = Sq_Circ holds
( (f . p) `2 >= 0 iff p `2 >= 0 )

let f be Function of (),(); :: thesis: ( f = Sq_Circ implies ( (f . p) `2 >= 0 iff p `2 >= 0 ) )
assume A1: f = Sq_Circ ; :: thesis: ( (f . p) `2 >= 0 iff p `2 >= 0 )
thus ( (f . p) `2 >= 0 implies p `2 >= 0 ) :: thesis: ( p `2 >= 0 implies (f . p) `2 >= 0 )
proof
assume A2: (f . p) `2 >= 0 ; :: thesis:
reconsider g = Sq_Circ " as Function of (),() by JGRAPH_3:29;
A3: dom f = the carrier of () by FUNCT_2:def 1;
set q = f . p;
now :: thesis: ( ( f . p = 0. () & (g . (f . p)) `2 >= 0 ) or ( f . p <> 0. () & (g . (f . p)) `2 >= 0 ) )
per cases ( f . p = 0. () or f . p <> 0. () ) ;
case f . p = 0. () ; :: thesis: (g . (f . p)) `2 >= 0
hence (g . (f . p)) `2 >= 0 by ; :: thesis: verum
end;
case A4: f . p <> 0. () ; :: thesis: (g . (f . p)) `2 >= 0
now :: thesis: ( ( ( ( (f . p) `2 <= (f . p) `1 & - ((f . p) `1) <= (f . p) `2 ) or ( (f . p) `2 >= (f . p) `1 & (f . p) `2 <= - ((f . p) `1) ) ) & (g . (f . p)) `2 >= 0 ) or ( not ( (f . p) `2 <= (f . p) `1 & - ((f . p) `1) <= (f . p) `2 ) & not ( (f . p) `2 >= (f . p) `1 & (f . p) `2 <= - ((f . p) `1) ) & (g . (f . p)) `2 >= 0 ) )
per cases ) `2 <= (f . p) `1 & - ((f . p) `1) <= (f . p) `2 ) or ( (f . p) `2 >= (f . p) `1 & (f . p) `2 <= - ((f . p) `1) ) or ( not ( (f . p) `2 <= (f . p) `1 & - ((f . p) `1) <= (f . p) `2 ) & not ( (f . p) `2 >= (f . p) `1 & (f . p) `2 <= - ((f . p) `1) ) ) ) ;
case ( ( (f . p) `2 <= (f . p) `1 & - ((f . p) `1) <= (f . p) `2 ) or ( (f . p) `2 >= (f . p) `1 & (f . p) `2 <= - ((f . p) `1) ) ) ; :: thesis: (g . (f . p)) `2 >= 0
then A5: g . (f . p) = |[(((f . p) `1) * (sqrt (1 + ((((f . p) `2) / ((f . p) `1)) ^2)))),(((f . p) `2) * (sqrt (1 + ((((f . p) `2) / ((f . p) `1)) ^2))))]| by ;
(((f . p) `2) / ((f . p) `1)) ^2 >= 0 by XREAL_1:63;
then sqrt (1 + ((((f . p) `2) / ((f . p) `1)) ^2)) > 0 by SQUARE_1:25;
hence (g . (f . p)) `2 >= 0 by ; :: thesis: verum
end;
case ( not ( (f . p) `2 <= (f . p) `1 & - ((f . p) `1) <= (f . p) `2 ) & not ( (f . p) `2 >= (f . p) `1 & (f . p) `2 <= - ((f . p) `1) ) ) ; :: thesis: (g . (f . p)) `2 >= 0
then A6: g . (f . p) = |[(((f . p) `1) * (sqrt (1 + ((((f . p) `1) / ((f . p) `2)) ^2)))),(((f . p) `2) * (sqrt (1 + ((((f . p) `1) / ((f . p) `2)) ^2))))]| by JGRAPH_3:28;
(((f . p) `1) / ((f . p) `2)) ^2 >= 0 by XREAL_1:63;
then sqrt (1 + ((((f . p) `1) / ((f . p) `2)) ^2)) > 0 by SQUARE_1:25;
hence (g . (f . p)) `2 >= 0 by ; :: thesis: verum
end;
end;
end;
hence (g . (f . p)) `2 >= 0 ; :: thesis: verum
end;
end;
end;
hence p `2 >= 0 by ; :: thesis: verum
end;
thus ( p `2 >= 0 implies (f . p) `2 >= 0 ) :: thesis: verum
proof
assume A7: p `2 >= 0 ; :: thesis: (f . p) `2 >= 0
now :: thesis: ( ( p = 0. () & (f . p) `2 >= 0 ) or ( p <> 0. () & (f . p) `2 >= 0 ) )
per cases ( p = 0. () or p <> 0. () ) ;
case p = 0. () ; :: thesis: (f . p) `2 >= 0
hence (f . p) `2 >= 0 by ; :: thesis: verum
end;
case A8: p <> 0. () ; :: thesis: (f . p) `2 >= 0
now :: thesis: ( ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & (f . p) `2 >= 0 ) or ( not ( p `2 <= p `1 & - (p `1) <= p `2 ) & not ( p `2 >= p `1 & p `2 <= - (p `1) ) & (f . p) `2 >= 0 ) )
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) `2 >= 0
then A9: f . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| by ;
((p `2) / (p `1)) ^2 >= 0 by XREAL_1:63;
then sqrt (1 + (((p `2) / (p `1)) ^2)) > 0 by SQUARE_1:25;
hence (f . p) `2 >= 0 by ; :: 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) `2 >= 0
then A10: f . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| by ;
((p `1) / (p `2)) ^2 >= 0 by XREAL_1:63;
then sqrt (1 + (((p `1) / (p `2)) ^2)) > 0 by SQUARE_1:25;
hence (f . p) `2 >= 0 by ; :: thesis: verum
end;
end;
end;
hence (f . p) `2 >= 0 ; :: thesis: verum
end;
end;
end;
hence (f . p) `2 >= 0 ; :: thesis: verum
end;