let x, y be real number ; :: thesis: ( x ^2 < 1 & y < 1 implies (x ^2 ) * y < 1 )
assume A1: ( x ^2 < 1 & y < 1 ) ; :: thesis: (x ^2 ) * y < 1

per cases ( 0 = x ^2 or 0 < x ^2 ) by XREAL_1:65;

suppose 0 = x ^2 ; :: thesis: (x ^2 ) * y < 1

hence (x ^2 ) * y < 1 ; :: thesis: verum

end;

suppose 0 < x ^2 ; :: thesis: (x ^2 ) * y < 1

then y * (x ^2 ) < 1 * (x ^2 ) by A1, XREAL_1:70;
hence (x ^2 ) * y < 1 by A1, XXREAL_0:2; :: thesis: verum

end;

end;