let h be Function of COMPLEX,COMPLEX; :: thesis: for g being Function of REAL,REAL

for y1 being FinSequence of COMPLEX

for y2 being FinSequence of REAL st len y1 = len y2 & ( for i being Element of NAT st i in dom y1 holds

h . (y1 . i) = g . (y2 . i) ) holds

h * y1 = g * y2

let g be Function of REAL,REAL; :: thesis: for y1 being FinSequence of COMPLEX

for y2 being FinSequence of REAL st len y1 = len y2 & ( for i being Element of NAT st i in dom y1 holds

h . (y1 . i) = g . (y2 . i) ) holds

h * y1 = g * y2

let y1 be FinSequence of COMPLEX ; :: thesis: for y2 being FinSequence of REAL st len y1 = len y2 & ( for i being Element of NAT st i in dom y1 holds

h . (y1 . i) = g . (y2 . i) ) holds

h * y1 = g * y2

let y2 be FinSequence of REAL ; :: thesis: ( len y1 = len y2 & ( for i being Element of NAT st i in dom y1 holds

h . (y1 . i) = g . (y2 . i) ) implies h * y1 = g * y2 )

assume that

A1: len y1 = len y2 and

A2: for i being Element of NAT st i in dom y1 holds

h . (y1 . i) = g . (y2 . i) ; :: thesis: h * y1 = g * y2

A3: len (g * y2) = len y1 by A1, FINSEQ_2:33;

for y1 being FinSequence of COMPLEX

for y2 being FinSequence of REAL st len y1 = len y2 & ( for i being Element of NAT st i in dom y1 holds

h . (y1 . i) = g . (y2 . i) ) holds

h * y1 = g * y2

let g be Function of REAL,REAL; :: thesis: for y1 being FinSequence of COMPLEX

for y2 being FinSequence of REAL st len y1 = len y2 & ( for i being Element of NAT st i in dom y1 holds

h . (y1 . i) = g . (y2 . i) ) holds

h * y1 = g * y2

let y1 be FinSequence of COMPLEX ; :: thesis: for y2 being FinSequence of REAL st len y1 = len y2 & ( for i being Element of NAT st i in dom y1 holds

h . (y1 . i) = g . (y2 . i) ) holds

h * y1 = g * y2

let y2 be FinSequence of REAL ; :: thesis: ( len y1 = len y2 & ( for i being Element of NAT st i in dom y1 holds

h . (y1 . i) = g . (y2 . i) ) implies h * y1 = g * y2 )

assume that

A1: len y1 = len y2 and

A2: for i being Element of NAT st i in dom y1 holds

h . (y1 . i) = g . (y2 . i) ; :: thesis: h * y1 = g * y2

A3: len (g * y2) = len y1 by A1, FINSEQ_2:33;

now :: thesis: for i being Nat st 1 <= i & i <= len (h * y1) holds

(h * y1) . i = (g * y2) . i

hence
h * y1 = g * y2
by A3, FINSEQ_2:33; :: thesis: verum(h * y1) . i = (g * y2) . i

let i be Nat; :: thesis: ( 1 <= i & i <= len (h * y1) implies (h * y1) . i = (g * y2) . i )

assume that

A4: 1 <= i and

A5: i <= len (h * y1) ; :: thesis: (h * y1) . i = (g * y2) . i

A6: i <= len y1 by A5, FINSEQ_2:33;

then A7: i in dom y1 by A4, FINSEQ_3:25;

A8: i in dom (g * y2) by A3, A4, A6, FINSEQ_3:25;

i in dom (h * y1) by A4, A5, FINSEQ_3:25;

hence (h * y1) . i = h . (y1 . i) by FUNCT_1:12

.= g . (y2 . i) by A2, A7

.= (g * y2) . i by A8, FUNCT_1:12 ;

:: thesis: verum

end;assume that

A4: 1 <= i and

A5: i <= len (h * y1) ; :: thesis: (h * y1) . i = (g * y2) . i

A6: i <= len y1 by A5, FINSEQ_2:33;

then A7: i in dom y1 by A4, FINSEQ_3:25;

A8: i in dom (g * y2) by A3, A4, A6, FINSEQ_3:25;

i in dom (h * y1) by A4, A5, FINSEQ_3:25;

hence (h * y1) . i = h . (y1 . i) by FUNCT_1:12

.= g . (y2 . i) by A2, A7

.= (g * y2) . i by A8, FUNCT_1:12 ;

:: thesis: verum