let b, c, d be Real; :: thesis: ( b < c implies (AffineMap ((d * (1 / (c - b))),(d * (- (b / (c - b)))))) + (AffineMap ((d * (- (1 / (c - b)))),(d * (c / (c - b))))) = AffineMap (0,d) )
assume A1: b < c ; :: thesis: (AffineMap ((d * (1 / (c - b))),(d * (- (b / (c - b)))))) + (AffineMap ((d * (- (1 / (c - b)))),(d * (c / (c - b))))) = AffineMap (0,d)
set f = AffineMap ((d * (1 / (c - b))),(d * (- (b / (c - b)))));
set g = AffineMap ((d * (- (1 / (c - b)))),(d * (c / (c - b))));
A2: dom ((AffineMap ((d * (1 / (c - b))),(d * (- (b / (c - b)))))) + (AffineMap ((d * (- (1 / (c - b)))),(d * (c / (c - b)))))) = (dom (AffineMap ((d * (1 / (c - b))),(d * (- (b / (c - b))))))) /\ (dom (AffineMap ((d * (- (1 / (c - b)))),(d * (c / (c - b)))))) by VALUED_1:def 1
.= (dom (AffineMap ((d * (1 / (c - b))),(d * (- (b / (c - b))))))) /\ REAL by FUNCT_2:def 1
.= REAL /\ REAL by FUNCT_2:def 1
.= dom (AffineMap (0,d)) by FUNCT_2:def 1 ;
for x being object st x in dom (AffineMap (0,d)) holds
((AffineMap ((d * (1 / (c - b))),(d * (- (b / (c - b)))))) + (AffineMap ((d * (- (1 / (c - b)))),(d * (c / (c - b)))))) . x = (AffineMap (0,d)) . x

proof

let x be object ; :: thesis: ( x in dom (AffineMap (0,d)) implies ((AffineMap ((d * (1 / (c - b))),(d * (- (b / (c - b)))))) + (AffineMap ((d * (- (1 / (c - b)))),(d * (c / (c - b)))))) . x = (AffineMap (0,d)) . x )
assume A3: x in dom (AffineMap (0,d)) ; :: thesis: ((AffineMap ((d * (1 / (c - b))),(d * (- (b / (c - b)))))) + (AffineMap ((d * (- (1 / (c - b)))),(d * (c / (c - b)))))) . x = (AffineMap (0,d)) . x
then reconsider x = x as Real ;
A5: c - b <> 0 by A1;
((AffineMap ((d * (1 / (c - b))),(d * (- (b / (c - b)))))) + (AffineMap ((d * (- (1 / (c - b)))),(d * (c / (c - b)))))) . x = ((AffineMap ((d * (1 / (c - b))),(d * (- (b / (c - b)))))) . x) + ((AffineMap ((d * (- (1 / (c - b)))),(d * (c / (c - b))))) . x) by VALUED_1:def 1, A2, A3
.= (((d * (1 / (c - b))) * x) + (d * (- (b / (c - b))))) + ((AffineMap ((d * (- (1 / (c - b)))),(d * (c / (c - b))))) . x) by FCONT_1:def 4
.= (((d * (1 / (c - b))) * x) + (d * (- (b / (c - b))))) + (((d * (- (1 / (c - b)))) * x) + (d * (c / (c - b)))) by FCONT_1:def 4
.= (0 * x) + (d * ((c / (c - b)) - (b / (c - b))))
.= (0 * x) + (d * ((c - b) / (c - b))) by XCMPLX_1:120
.= (0 * x) + (d * 1) by XCMPLX_1:60, A5 ;
hence ((AffineMap ((d * (1 / (c - b))),(d * (- (b / (c - b)))))) + (AffineMap ((d * (- (1 / (c - b)))),(d * (c / (c - b)))))) . x = (AffineMap (0,d)) . x by FCONT_1:def 4; :: thesis: verum

end;

hence (AffineMap ((d * (1 / (c - b))),(d * (- (b / (c - b)))))) + (AffineMap ((d * (- (1 / (c - b)))),(d * (c / (c - b))))) = AffineMap (0,d) by A2, FUNCT_1:2; :: thesis: verum