let A, B, C, D be Real; :: thesis: ( A > 0 & C > 0 implies AffineMap (A,B,C,D) is onto )
assume A1: ( A > 0 & C > 0 ) ; :: thesis: AffineMap (A,B,C,D) is onto
thus rng (AffineMap (A,B,C,D)) c= the carrier of (TOP-REAL 2) ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of (TOP-REAL 2) c= rng (AffineMap (A,B,C,D))
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in the carrier of (TOP-REAL 2) or e in rng (AffineMap (A,B,C,D)) )
assume e in the carrier of (TOP-REAL 2) ; :: thesis: e in rng (AffineMap (A,B,C,D))
then reconsider q1 = e as Point of (TOP-REAL 2) ;
set q2 = (AffineMap ((1 / A),(- (B / A)),(1 / C),(- (D / C)))) . q1;
A2: the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22;
(AffineMap (A,B,C,D)) . ((AffineMap ((1 / A),(- (B / A)),(1 / C),(- (D / C)))) . q1) = ((AffineMap (A,B,C,D)) * (AffineMap ((1 / A),(- (B / A)),(1 / C),(- (D / C))))) . q1 by FUNCT_2:15
.= (id (REAL 2)) . q1 by A1, Th34
.= q1 by A2 ;
hence e in rng (AffineMap (A,B,C,D)) by FUNCT_2:4; :: thesis: verum