let A, B be complex-membered set ; for a being Complex st a <> 0 holds
(A \+\ B) /// a = (A /// a) \+\ (B /// a)
let a be Complex; ( a <> 0 implies (A \+\ B) /// a = (A /// a) \+\ (B /// a) )
assume A1:
a <> 0
; (A \+\ B) /// a = (A /// a) \+\ (B /// a)
A2:
{a} "" = {(a ")}
by Th37;
thus (A \+\ B) /// a =
(a ") ** (A \+\ B)
by Th37
.=
((a ") ** A) \+\ ((a ") ** B)
by A1, Th200
.=
(A /// a) \+\ (B /// a)
by A2
; verum