let A, B, C, A1, B1, C1 be Point of (TOP-REAL 2); :: thesis: for lambda, mu, nu being Real st A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C1 = ((1 - nu) * A) + (nu * B) holds
the_area_of_polygon3 (A1,B1,C1) = ((((1 - lambda) * (1 - mu)) * (1 - nu)) + ((lambda * mu) * nu)) * (the_area_of_polygon3 (A,B,C))
let lambda, mu, nu be Real; :: thesis: ( A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C1 = ((1 - nu) * A) + (nu * B) implies the_area_of_polygon3 (A1,B1,C1) = ((((1 - lambda) * (1 - mu)) * (1 - nu)) + ((lambda * mu) * nu)) * (the_area_of_polygon3 (A,B,C)) )
assume that
A1: A1 = ((1 - lambda) * B) + (lambda * C) and
A2: B1 = ((1 - mu) * C) + (mu * A) and
A3: C1 = ((1 - nu) * A) + (nu * B) ; :: thesis: the_area_of_polygon3 (A1,B1,C1) = ((((1 - lambda) * (1 - mu)) * (1 - nu)) + ((lambda * mu) * nu)) * (the_area_of_polygon3 (A,B,C))
the_area_of_polygon3 (A1,B1,C1) = ((1 - lambda) * (the_area_of_polygon3 (B,B1,C1))) + (lambda * (the_area_of_polygon3 (C,B1,C1))) by Th7, A1
.= (- ((1 - lambda) * (the_area_of_polygon3 ((((1 - mu) * C) + (mu * A)),B,C1)))) - (lambda * (the_area_of_polygon3 ((((1 - mu) * C) + (mu * A)),C,C1))) by A2
.= (- ((1 - lambda) * (((1 - mu) * (the_area_of_polygon3 (C,B,C1))) + (mu * (the_area_of_polygon3 (A,B,C1)))))) - (lambda * (the_area_of_polygon3 ((((1 - mu) * C) + (mu * A)),C,C1))) by Th7
.= (- ((1 - lambda) * (((1 - mu) * (the_area_of_polygon3 (C,B,C1))) + (mu * (the_area_of_polygon3 (A,B,C1)))))) - (lambda * (((1 - mu) * (the_area_of_polygon3 (C,C,C1))) + (mu * (the_area_of_polygon3 (A,C,C1))))) by Th7
.= ((((1 - lambda) * (1 - mu)) * (the_area_of_polygon3 ((((1 - nu) * A) + (nu * B)),B,C))) + (((1 - lambda) * mu) * (the_area_of_polygon3 ((((1 - nu) * A) + (nu * B)),B,A)))) + ((lambda * mu) * (the_area_of_polygon3 ((((1 - nu) * A) + (nu * B)),C,A))) by A3
.= ((((1 - lambda) * (1 - mu)) * (((1 - nu) * (the_area_of_polygon3 (A,B,C))) + (nu * (the_area_of_polygon3 (B,B,C))))) + (((1 - lambda) * mu) * (the_area_of_polygon3 ((((1 - nu) * A) + (nu * B)),B,A)))) + ((lambda * mu) * (the_area_of_polygon3 ((((1 - nu) * A) + (nu * B)),C,A))) by Th7
.= (((((1 - lambda) * (1 - mu)) * (1 - nu)) * (the_area_of_polygon3 (A,B,C))) + (((1 - lambda) * mu) * (((1 - nu) * (the_area_of_polygon3 (A,B,A))) + (nu * (the_area_of_polygon3 (B,B,A)))))) + ((lambda * mu) * (the_area_of_polygon3 ((((1 - nu) * A) + (nu * B)),C,A))) by Th7
.= ((((1 - lambda) * (1 - mu)) * (1 - nu)) * (the_area_of_polygon3 (A,B,C))) + ((lambda * mu) * (((1 - nu) * (the_area_of_polygon3 (A,C,A))) + (nu * (the_area_of_polygon3 (B,C,A))))) by Th7 ;
hence the_area_of_polygon3 (A1,B1,C1) = ((((1 - lambda) * (1 - mu)) * (1 - nu)) + ((lambda * mu) * nu)) * (the_area_of_polygon3 (A,B,C)) ; :: thesis: verum