let A, B be complex-membered set ; :: thesis: for a being complex number holds (A ++ B) /// a = (A /// a) ++ (B /// a)
let a be complex number ; :: thesis: (A ++ B) /// a = (A /// a) ++ (B /// a)
thus (A ++ B) /// a = (a ") ** (A ++ B) by Th37
.= ((a ") ** A) ++ ((a ") ** B) by Th208
.= (A /// a) ++ ((a ") ** B) by Th37
.= (A /// a) ++ (B /// a) by Th37 ; :: thesis: verum