let a, b be real number ; :: thesis: ( a <> 0 implies (AffineMap a,b) " = AffineMap (a " ),(- (b / a)) )
assume A1: a <> 0 ; :: thesis: (AffineMap a,b) " = AffineMap (a " ),(- (b / a))
A2: rng (AffineMap a,b) = REAL by A1, Th32;
for x being Element of REAL holds ((AffineMap (a " ),(- (b / a))) * (AffineMap a,b)) . x = (id REAL ) . x

proof

let x be Element of REAL ; :: thesis: ((AffineMap (a " ),(- (b / a))) * (AffineMap a,b)) . x = (id REAL ) . x
thus ((AffineMap (a " ),(- (b / a))) * (AffineMap a,b)) . x = (AffineMap (a " ),(- (b / a))) . ((AffineMap a,b) . x) by FUNCT_2:21
.= (AffineMap (a " ),(- (b / a))) . ((a * x) + b) by Def3
.= ((a " ) * ((a * x) + b)) + (- (b / a)) by Def3
.= ((((a " ) * a) * x) + ((a " ) * b)) + (- (b / a))
.= ((1 * x) + ((a " ) * b)) + (- (b / a)) by A1, XCMPLX_0:def 7
.= (x + ((a " ) * b)) - (b / a)
.= (x + (b / a)) - (b / a) by XCMPLX_0:def 9
.= (id REAL ) . x by FUNCT_1:35 ; :: thesis: verum

end;

then (AffineMap (a " ),(- (b / a))) * (AffineMap a,b) = id REAL by FUNCT_2:113;
hence (AffineMap a,b) " = AffineMap (a " ),(- (b / a)) by A1, A2, Th27, FUNCT_2:36; :: thesis: verum