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 A1: ( len y1 = len y2 & ( for i being Element of NAT st i in dom y1 holds
h . (y1 . i) = g . (y2 . i) ) ) ; :: thesis: h * y1 = g * y2
A2: len (h * y1) = len y1 by FINSEQ_2:37;
A3: len (g * y2) = len y1 by A1, FINSEQ_2:37;

now

let i be Nat; :: thesis: ( 1 <= i & i <= len (h * y1) implies (h * y1) . i = (g * y2) . i )
assume A4: ( 1 <= i & i <= len (h * y1) ) ; :: thesis: (h * y1) . i = (g * y2) . i
then A5: ( 1 <= i & i <= len y1 ) by FINSEQ_2:37;
then A6: i in dom y1 by FINSEQ_3:27;
A7: i in dom (g * y2) by A3, A5, FINSEQ_3:27;
i in dom (h * y1) by A4, FINSEQ_3:27;
hence (h * y1) . i = h . (y1 . i) by FUNCT_1:22
.= g . (y2 . i) by A1, A6
.= (g * y2) . i by A7, FUNCT_1:22 ;
:: thesis: verum

end;

hence h * y1 = g * y2 by A2, A3, FINSEQ_1:18; :: thesis: verum