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 ;
A9: len (y - (y *')) = len y by ;
thus Re (x + y) = (1 / 2) * ((x + y) + ((x *') + (y *'))) by
.= (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
.= (- ((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