let cn be Real; :: thesis: for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 >= 0 holds
for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds
p `2 >= 0
let q be Point of (TOP-REAL 2); :: thesis: ( - 1 < cn & cn < 1 & q `2 >= 0 implies for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds
p `2 >= 0 )
assume that
A1: ( - 1 < cn & cn < 1 ) and
A2: q `2 >= 0 ; :: thesis: for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds
p `2 >= 0

now

per cases ( q `2 > 0 or q `2 = 0 ) by A2;

case q `2 > 0 ; :: thesis: for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds
p `2 >= 0

hence for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds
p `2 >= 0 by A1, Th21; :: thesis: verum

end;

case q `2 = 0 ; :: thesis: for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds
p `2 >= 0

hence for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds
p `2 >= 0 by JGRAPH_4:56; :: thesis: verum

end;

end;

end;

hence for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds
p `2 >= 0 ; :: thesis: verum