let a, b be Real; :: thesis: ( a <> 0 implies (AffineMap (a,b)) " = AffineMap ((a "),(- (b / a))) )
assume A1: a <> 0 ; :: thesis: (AffineMap (a,b)) " = AffineMap ((a "),(- (b / a)))
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:15
.= (AffineMap ((a "),(- (b / a)))) . ((a * x) + b) by Def4
.= ((a ") * ((a * x) + b)) + (- (b / a)) by Def4
.= ((((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 ; :: thesis: verum
end;
then A2: (AffineMap ((a "),(- (b / a)))) * (AffineMap (a,b)) = id REAL by FUNCT_2:63;
rng (AffineMap (a,b)) = REAL by A1, Th55;
hence (AffineMap (a,b)) " = AffineMap ((a "),(- (b / a))) by A1, A2, Th50, FUNCT_2:30; :: thesis: verum