let A, B, C, A1 be Point of (TOP-REAL 2); :: thesis: for lambda being Real holds the_area_of_polygon3 ((((1 - lambda) * A) + (lambda * A1)),B,C) = ((1 - lambda) * (the_area_of_polygon3 (A,B,C))) + (lambda * (the_area_of_polygon3 (A1,B,C)))
let lambda be Real; :: thesis: the_area_of_polygon3 ((((1 - lambda) * A) + (lambda * A1)),B,C) = ((1 - lambda) * (the_area_of_polygon3 (A,B,C))) + (lambda * (the_area_of_polygon3 (A1,B,C)))
the_area_of_polygon3 ((((1 - lambda) * A) + (lambda * A1)),B,C) = (((((((1 - lambda) * (A `1)) + (lambda * (A1 `1))) * (B `2)) - ((B `1) * ((((1 - lambda) * A) + (lambda * A1)) `2))) + (((B `1) * (C `2)) - ((C `1) * (B `2)))) + (((C `1) * ((((1 - lambda) * A) + (lambda * A1)) `2)) - (((((1 - lambda) * A) + (lambda * A1)) `1) * (C `2)))) / 2 by Th4
.= (((((((1 - lambda) * (A `1)) + (lambda * (A1 `1))) * (B `2)) - ((B `1) * (((1 - lambda) * (A `2)) + (lambda * (A1 `2))))) + (((B `1) * (C `2)) - ((C `1) * (B `2)))) + (((C `1) * ((((1 - lambda) * A) + (lambda * A1)) `2)) - (((((1 - lambda) * A) + (lambda * A1)) `1) * (C `2)))) / 2 by Th4
.= (((((((1 - lambda) * (A `1)) + (lambda * (A1 `1))) * (B `2)) - ((B `1) * (((1 - lambda) * (A `2)) + (lambda * (A1 `2))))) + (((B `1) * (C `2)) - ((C `1) * (B `2)))) + (((C `1) * (((1 - lambda) * (A `2)) + (lambda * (A1 `2)))) - (((((1 - lambda) * A) + (lambda * A1)) `1) * (C `2)))) / 2 by Th4
.= (((((((1 - lambda) * (A `1)) + (lambda * (A1 `1))) * (B `2)) - ((B `1) * (((1 - lambda) * (A `2)) + (lambda * (A1 `2))))) + (((B `1) * (C `2)) - ((C `1) * (B `2)))) + (((C `1) * (((1 - lambda) * (A `2)) + (lambda * (A1 `2)))) - ((((1 - lambda) * (A `1)) + (lambda * (A1 `1))) * (C `2)))) / 2 by Th4 ;
hence the_area_of_polygon3 ((((1 - lambda) * A) + (lambda * A1)),B,C) = ((1 - lambda) * (the_area_of_polygon3 (A,B,C))) + (lambda * (the_area_of_polygon3 (A1,B,C))) ; :: thesis: verum