let x, y1, y2 be FinSequence of COMPLEX ; ( len x = len y1 & len y1 = len y2 implies |(x,(y1 - y2))| = |(x,y1)| - |(x,y2)| )
assume that
A1:
len x = len y1
and
A2:
len y1 = len y2
; |(x,(y1 - y2))| = |(x,y1)| - |(x,y2)|
A3:
( len (Re y1) = len y1 & len (Re y2) = len y2 )
by Th40;
A4:
len (Im x) = len x
by Th40;
A5:
( len (Im y1) = len y1 & len (Im y2) = len y2 )
by Th40;
A6:
len (Re x) = len x
by Th40;
|(x,(y1 - y2))| =
((|((Re x),((Re y1) - (Re y2)))| - (<i> * |((Re x),(Im (y1 - y2)))|)) + (<i> * |((Im x),(Re (y1 - y2)))|)) + |((Im x),(Im (y1 - y2)))|
by A2, Th43
.=
((|((Re x),((Re y1) - (Re y2)))| - (<i> * |((Re x),(Im (y1 - y2)))|)) + (<i> * |((Im x),(Re (y1 - y2)))|)) + |((Im x),((Im y1) - (Im y2)))|
by A2, Th43
.=
((|((Re x),((Re y1) - (Re y2)))| - (<i> * |((Re x),((Im y1) - (Im y2)))|)) + (<i> * |((Im x),(Re (y1 - y2)))|)) + |((Im x),((Im y1) - (Im y2)))|
by A2, Th43
.=
((|((Re x),((Re y1) - (Re y2)))| - (<i> * |((Re x),((Im y1) - (Im y2)))|)) + (<i> * |((Im x),((Re y1) - (Re y2)))|)) + |((Im x),((Im y1) - (Im y2)))|
by A2, Th43
.=
(((|((Re x),(Re y1))| - |((Re x),(Re y2))|) - (<i> * |((Re x),((Im y1) - (Im y2)))|)) + (<i> * |((Im x),((Re y1) - (Re y2)))|)) + |((Im x),((Im y1) - (Im y2)))|
by A1, A2, A3, A6, RVSUM_1:124
.=
(((|((Re x),(Re y1))| - |((Re x),(Re y2))|) - (<i> * |((Re x),((Im y1) - (Im y2)))|)) + (<i> * |((Im x),((Re y1) - (Re y2)))|)) + (|((Im x),(Im y1))| - |((Im x),(Im y2))|)
by A1, A2, A5, A4, RVSUM_1:124
.=
(((|((Re x),(Re y1))| - |((Re x),(Re y2))|) - (<i> * (|((Re x),(Im y1))| - |((Re x),(Im y2))|))) + (<i> * |((Im x),((Re y1) - (Re y2)))|)) + (|((Im x),(Im y1))| - |((Im x),(Im y2))|)
by A1, A2, A6, A5, RVSUM_1:124
.=
(((|((Re x),(Re y1))| - |((Re x),(Re y2))|) - (<i> * (|((Re x),(Im y1))| - |((Re x),(Im y2))|))) + (<i> * (|((Im x),(Re y1))| - |((Im x),(Re y2))|))) + (|((Im x),(Im y1))| - |((Im x),(Im y2))|)
by A1, A2, A3, A4, RVSUM_1:124
.=
|(x,y1)| - |(x,y2)|
;
hence
|(x,(y1 - y2))| = |(x,y1)| - |(x,y2)|
; verum