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) ) )
assume A1: len x = len y ; :: thesis: ( Re (x - y) = (Re x) - (Re y) & Im (x - y) = (Im x) - (Im y) )
then A2: len (x - y) = len x by Th7;
A3: len x = len (x *') by Def1;
then A4: len (x + (x *')) = len x by Th6;
A5: len y = len (y *') by Def1;
then A6: len (y + (y *')) = len y by Th6;
thus Re (x - y) = (1 / 2) * ((x - y) + ((x *') - (y *'))) by A1, Th17
.= (1 / 2) * (((x *') + (x - y)) - (y *')) by A1, A5, A3, A2, Th31
.= (1 / 2) * ((x *') + ((x - y) - (y *'))) by A1, A5, A3, A2, Th31
.= (1 / 2) * ((x *') + (x - (y + (y *')))) by A1, A5, Th30
.= (1 / 2) * ((x + (x *')) - (y + (y *'))) by A1, A3, A6, Th31
.= (Re x) - (Re y) by A1, A4, A6, Th36 ; :: thesis: Im (x - y) = (Im x) - (Im y)
A7: len (x - (x *')) = len x by A3, Th7;
A8: len (y - (y *')) = len y by A5, Th7;
thus Im (x - y) = (- ((1 / 2) * <i>)) * ((x - y) - ((x *') - (y *'))) by A1, Th17
.= (- ((1 / 2) * <i>)) * (((x - y) - (x *')) + (y *')) by A1, A5, A3, A2, Th33
.= (- ((1 / 2) * <i>)) * ((x - ((x *') + y)) + (y *')) by A1, A3, Th30
.= (- ((1 / 2) * <i>)) * (((x - (x *')) - y) + (y *')) by A1, A3, Th30
.= (- ((1 / 2) * <i>)) * ((x - (x *')) - (y - (y *'))) by A1, A5, A7, Th33
.= (Im x) - (Im y) by A1, A7, A8, Th36 ; :: thesis: verum