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) ) )
assume A1:
len x = len y
; ( 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, Th21
.=
(1 / 2) * (((x *' ) + (x - y)) - (y *' ))
by A1, A5, A3, A2, Th37
.=
(1 / 2) * ((x *' ) + ((x - y) - (y *' )))
by A1, A5, A3, A2, Th37
.=
(1 / 2) * ((x *' ) + (x - (y + (y *' ))))
by A1, A5, Th36
.=
(1 / 2) * ((x + (x *' )) - (y + (y *' )))
by A1, A3, A6, Th37
.=
(Re x) - (Re y)
by A1, A4, A6, Th43
; 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, Th21
.=
(- ((1 / 2) * <i> )) * (((x - y) - (x *' )) + (y *' ))
by A1, A5, A3, A2, Th40
.=
(- ((1 / 2) * <i> )) * ((x - ((x *' ) + y)) + (y *' ))
by A1, A3, Th36
.=
(- ((1 / 2) * <i> )) * (((x - (x *' )) - y) + (y *' ))
by A1, A3, Th36
.=
(- ((1 / 2) * <i> )) * ((x - (x *' )) - (y - (y *' )))
by A1, A5, A7, Th40
.=
(Im x) - (Im y)
by A1, A7, A8, Th43
; verum