let A, B, C, D be Real; ( A > 0 & C > 0 implies AffineMap (A,B,C,D) is onto )
assume A1:
( A > 0 & C > 0 )
; AffineMap (A,B,C,D) is onto
thus
rng (AffineMap (A,B,C,D)) c= the carrier of (TOP-REAL 2)
; XBOOLE_0:def 10,FUNCT_2:def 3 the carrier of (TOP-REAL 2) c= rng (AffineMap (A,B,C,D))
let e be object ; TARSKI:def 3 ( 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)
; 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; verum