let x, y be FinSequence of COMPLEX ; :: thesis: ( 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 ; :: thesis: ( 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, Th15

.= (1 / 2) * (((x + y) + (x *')) + (y *')) by A2, A4, A6, A3, Th24

.= (1 / 2) * (((x + (x *')) + y) + (y *')) by A2, A6, Th24

.= (1 / 2) * ((x + (x *')) + (y + (y *'))) by A2, A4, A7, Th24

.= (Re x) + (Re y) by A2, A7, A5, Th25 ; :: thesis: Im (x + y) = (Im x) + (Im y)

thus Im (x + y) = (- ((1 / 2) * <i>)) * ((x + y) - ((x *') + (y *'))) by A2, Th15

.= (- ((1 / 2) * <i>)) * (((x + y) - (x *')) - (y *')) by A2, A4, A6, A3, Th30

.= (- ((1 / 2) * <i>)) * (((x + (- (x *'))) + y) - (y *')) by A2, A6, A1, Th24

.= (- ((1 / 2) * <i>)) * ((x - (x *')) + (y - (y *'))) by A2, A4, A8, Th31

.= (Im x) + (Im y) by A2, A8, A9, Th25 ; :: thesis: verum

A1: len (- (x *')) = len (x *') by Th5;

assume A2: len x = len y ; :: thesis: ( 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, Th15

.= (1 / 2) * (((x + y) + (x *')) + (y *')) by A2, A4, A6, A3, Th24

.= (1 / 2) * (((x + (x *')) + y) + (y *')) by A2, A6, Th24

.= (1 / 2) * ((x + (x *')) + (y + (y *'))) by A2, A4, A7, Th24

.= (Re x) + (Re y) by A2, A7, A5, Th25 ; :: thesis: Im (x + y) = (Im x) + (Im y)

thus Im (x + y) = (- ((1 / 2) * <i>)) * ((x + y) - ((x *') + (y *'))) by A2, Th15

.= (- ((1 / 2) * <i>)) * (((x + y) - (x *')) - (y *')) by A2, A4, A6, A3, Th30

.= (- ((1 / 2) * <i>)) * (((x + (- (x *'))) + y) - (y *')) by A2, A6, A1, Th24

.= (- ((1 / 2) * <i>)) * ((x - (x *')) + (y - (y *'))) by A2, A4, A8, Th31

.= (Im x) + (Im y) by A2, A8, A9, Th25 ; :: thesis: verum