let x, y be FinSequence of COMPLEX ; ( len x = len y implies ( Re (x + y) = (Re x) + (Re y) & Im (x + y) = (Im x) + (Im y) ) )
A1:
len (- (x *' )) = len (x *' )
by Th5;
assume A2:
len x = len y
; ( Re (x + y) = (Re x) + (Re y) & Im (x + y) = (Im x) + (Im y) )
then A3:
len (x + y) = len x
by Th6;
A4:
len y = len (y *' )
by Def1;
then A5:
len (y + (y *' )) = len y
by Th6;
A6:
len x = len (x *' )
by Def1;
then A7:
len (x + (x *' )) = len x
by Th6;
A8:
len (x - (x *' )) = len x
by A6, Th7;
A9:
len (y - (y *' )) = len y
by A4, Th7;
thus Re (x + y) =
(1 / 2) * ((x + y) + ((x *' ) + (y *' )))
by A2, Th19
.=
(1 / 2) * (((x + y) + (x *' )) + (y *' ))
by A2, A4, A6, A3, Th28
.=
(1 / 2) * (((x + (x *' )) + y) + (y *' ))
by A2, A6, Th28
.=
(1 / 2) * ((x + (x *' )) + (y + (y *' )))
by A2, A4, A7, Th28
.=
(Re x) + (Re y)
by A2, A7, A5, Th30
; Im (x + y) = (Im x) + (Im y)
thus Im (x + y) =
(- ((1 / 2) * <i> )) * ((x + y) - ((x *' ) + (y *' )))
by A2, Th19
.=
(- ((1 / 2) * <i> )) * (((x + y) - (x *' )) - (y *' ))
by A2, A4, A6, A3, Th36
.=
(- ((1 / 2) * <i> )) * (((x + (- (x *' ))) + y) - (y *' ))
by A2, A6, A1, Th28
.=
(- ((1 / 2) * <i> )) * ((x - (x *' )) + (y - (y *' )))
by A2, A4, A8, Th37
.=
(Im x) + (Im y)
by A2, A8, A9, Th30
; verum