let p, q, s, t be Real; for f being Function of REAL,REAL st p * s < 0 & p > 0 & ((p * t) - (q * s)) / (p - s) > 0 holds
((AffineMap (p,q)) | [.(- (q / p)),((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),(- (t / s)).]) = (((p * t) - (q * s)) / (p - s)) (#) ((TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s)))) | [.(- (q / p)),(- (t / s)).])
let f be Function of REAL,REAL; ( p * s < 0 & p > 0 & ((p * t) - (q * s)) / (p - s) > 0 implies ((AffineMap (p,q)) | [.(- (q / p)),((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),(- (t / s)).]) = (((p * t) - (q * s)) / (p - s)) (#) ((TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s)))) | [.(- (q / p)),(- (t / s)).]) )
assume that
A2:
( p * s < 0 & p > 0 )
and
A3:
((p * t) - (q * s)) / (p - s) > 0
; ((AffineMap (p,q)) | [.(- (q / p)),((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),(- (t / s)).]) = (((p * t) - (q * s)) / (p - s)) (#) ((TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s)))) | [.(- (q / p)),(- (t / s)).])
set r = ((p * t) - (q * s)) / (p - s);
set b = (t - q) / (p - s);
set f = (((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))));
A7:
p - s <> 0
by A2;
A4:
for x being Real holds ((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x = ((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x
;
A8: ((t - q) / (p - s)) + (q / p) =
(((t - q) * p) + (q * (p - s))) / ((p - s) * p)
by XCMPLX_1:116, A7, A2
.=
(1 / p) * (((t * p) - (q * s)) / (p - s))
by XCMPLX_1:103
;
A5:
- (q / p) < (t - q) / (p - s)
by Th13, A2, A3;
A9:
s < 0
by A2;
then A10: ((t - q) / (p - s)) + (t / s) =
(((t - q) * s) + (t * (p - s))) / ((p - s) * s)
by XCMPLX_1:116, A2
.=
(1 / s) * (((t * p) - (q * s)) / (p - s))
by XCMPLX_1:103
;
A6:
(t - q) / (p - s) < - (t / s)
by Th13, A2, A3;
A11:
- (q / p) < - (t / s)
by Th13, A2, A3;
B1: (((p * t) - (q * s)) / (p - s)) * (1 / (((t - q) / (p - s)) - (- (q / p)))) =
(((p * t) - (q * s)) / (p - s)) * (1 / ((((p * t) - (q * s)) / (p - s)) / p))
by XCMPLX_1:99, A8
.=
(((p * t) - (q * s)) / (p - s)) * (p / (((p * t) - (q * s)) / (p - s)))
by XCMPLX_1:57
.=
p
by XCMPLX_1:87, A3
;
B2: (((p * t) - (q * s)) / (p - s)) * (- ((- (q / p)) / (((t - q) / (p - s)) - (- (q / p))))) =
(((p * t) - (q * s)) / (p - s)) * (- ((- (q / p)) / ((((p * t) - (q * s)) / (p - s)) / p)))
by XCMPLX_1:99, A8
.=
- ((((p * t) - (q * s)) / (p - s)) * ((- (q / p)) / ((((p * t) - (q * s)) / (p - s)) / p)))
.=
- ((((p * t) - (q * s)) / (p - s)) * (- ((q / p) / ((((p * t) - (q * s)) / (p - s)) / p))))
by XCMPLX_1:187
.=
(((p * t) - (q * s)) / (p - s)) * ((q / p) / ((((p * t) - (q * s)) / (p - s)) / p))
.=
(((p * t) - (q * s)) / (p - s)) * (q / (((p * t) - (q * s)) / (p - s)))
by XCMPLX_1:55, A2
.=
q
by XCMPLX_1:87, A3
;
B3: (((p * t) - (q * s)) / (p - s)) * (- (1 / ((- (t / s)) - ((t - q) / (p - s))))) =
(((p * t) - (q * s)) / (p - s)) * (- (1 / (- ((t / s) + ((t - q) / (p - s))))))
.=
(((p * t) - (q * s)) / (p - s)) * (- (- (1 / ((1 / s) * (((p * t) - (q * s)) / (p - s))))))
by XCMPLX_1:188, A10
.=
(((p * t) - (q * s)) / (p - s)) * (1 / ((((p * t) - (q * s)) / (p - s)) / s))
by XCMPLX_1:99
.=
(((p * t) - (q * s)) / (p - s)) * (s / (((p * t) - (q * s)) / (p - s)))
by XCMPLX_1:57
.=
s
by XCMPLX_1:87, A3
;
B4: (((p * t) - (q * s)) / (p - s)) * ((- (t / s)) / ((- (t / s)) - ((t - q) / (p - s)))) =
(((p * t) - (q * s)) / (p - s)) * ((- (t / s)) / (- ((t / s) + ((t - q) / (p - s)))))
.=
(((p * t) - (q * s)) / (p - s)) * (- ((- (t / s)) / ((1 / s) * (((p * t) - (q * s)) / (p - s)))))
by XCMPLX_1:188, A10
.=
(((p * t) - (q * s)) / (p - s)) * (- ((- (t / s)) / ((((p * t) - (q * s)) / (p - s)) / s)))
by XCMPLX_1:99
.=
(((p * t) - (q * s)) / (p - s)) * (- (- ((t / s) / ((((p * t) - (q * s)) / (p - s)) / s))))
by XCMPLX_1:187
.=
(((p * t) - (q * s)) / (p - s)) * (t / (((p * t) - (q * s)) / (p - s)))
by XCMPLX_1:55, A9
.=
t
by XCMPLX_1:87, A3
;
(((p * t) - (q * s)) / (p - s)) (#) ((TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s)))) | [.(- (q / p)),(- (t / s)).]) =
(((p * t) - (q * s)) / (p - s)) (#) ((TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s)))) | ['(- (q / p)),(- (t / s))'])
by INTEGRA5:def 3, A11
.=
((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) | ['(- (q / p)),(- (t / s))']
by FUZZY_7:10
.=
((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) | [.(- (q / p)),(- (t / s)).]
by INTEGRA5:def 3, A11
.=
(((((p * t) - (q * s)) / (p - s)) (#) (AffineMap ((1 / (((t - q) / (p - s)) - (- (q / p)))),(- ((- (q / p)) / (((t - q) / (p - s)) - (- (q / p)))))))) | [.(- (q / p)),((t - q) / (p - s)).]) +* (((((p * t) - (q * s)) / (p - s)) (#) (AffineMap ((- (1 / ((- (t / s)) - ((t - q) / (p - s))))),((- (t / s)) / ((- (t / s)) - ((t - q) / (p - s))))))) | [.((t - q) / (p - s)),(- (t / s)).])
by A4, A5, A6, Th7
.=
(((((p * t) - (q * s)) / (p - s)) (#) (AffineMap ((1 / (((t - q) / (p - s)) - (- (q / p)))),(- ((- (q / p)) / (((t - q) / (p - s)) - (- (q / p)))))))) | [.(- (q / p)),((t - q) / (p - s)).]) +* ((AffineMap (((((p * t) - (q * s)) / (p - s)) * (- (1 / ((- (t / s)) - ((t - q) / (p - s)))))),((((p * t) - (q * s)) / (p - s)) * ((- (t / s)) / ((- (t / s)) - ((t - q) / (p - s))))))) | [.((t - q) / (p - s)),(- (t / s)).])
by FUZZY_7:13
.=
((AffineMap (p,q)) | [.(- (q / p)),((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),(- (t / s)).])
by B1, B2, B3, B4, FUZZY_7:13
;
hence
((AffineMap (p,q)) | [.(- (q / p)),((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),(- (t / s)).]) = (((p * t) - (q * s)) / (p - s)) (#) ((TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s)))) | [.(- (q / p)),(- (t / s)).])
; verum