let K be Field; :: thesis: for f, g being FinSequence of NAT holds 1. (K,(f ^ g)) = (1. (K,f)) ^ (1. (K,g))
let f, g be FinSequence of NAT ; :: thesis: 1. (K,(f ^ g)) = (1. (K,f)) ^ (1. (K,g))
set F = 1. (K,f);
set G = 1. (K,g);
set FG = (1. (K,f)) ^ (1. (K,g));
set ONE = 1. (K,(f ^ g));
A1: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
A2: dom (1. (K,(f ^ g))) = dom (f ^ g) by Def8;
A3: dom (1. (K,g)) = dom g by Def8;
then A4: len (1. (K,g)) = len g by FINSEQ_3:29;
A5: dom (1. (K,f)) = dom f by Def8;
then A6: len (1. (K,f)) = len f by FINSEQ_3:29;
A7: len ((1. (K,f)) ^ (1. (K,g))) = (len (1. (K,f))) + (len (1. (K,g))) by FINSEQ_1:22;

A8: now :: thesis: for i being Nat st 1 <= i & i <= len ((1. (K,f)) ^ (1. (K,g))) holds
(1. (K,(f ^ g))) . i = ((1. (K,f)) ^ (1. (K,g))) . i

let i be Nat; :: thesis: ( 1 <= i & i <= len ((1. (K,f)) ^ (1. (K,g))) implies (1. (K,(f ^ g))) . i = ((1. (K,f)) ^ (1. (K,g))) . i )
assume that
A9: 1 <= i and
A10: i <= len ((1. (K,f)) ^ (1. (K,g))) ; :: thesis: (1. (K,(f ^ g))) . i = ((1. (K,f)) ^ (1. (K,g))) . i
i in dom (1. (K,(f ^ g))) by A2, A6, A4, A7, A1, A9, A10, FINSEQ_3:25;
then A11: (1. (K,(f ^ g))) . i = 1. (K,((f ^ g) . i)) by Def8;
A12: i in dom ((1. (K,f)) ^ (1. (K,g))) by A9, A10, FINSEQ_3:25;

now :: thesis: (1. (K,(f ^ g))) . i = ((1. (K,f)) ^ (1. (K,g))) . i

per cases ( i in dom (1. (K,f)) or ex n being Nat st
( n in dom (1. (K,g)) & i = (len (1. (K,f))) + n ) ) by A12, FINSEQ_1:25;

suppose A13: i in dom (1. (K,f)) ; :: thesis: (1. (K,(f ^ g))) . i = ((1. (K,f)) ^ (1. (K,g))) . i

hence (1. (K,(f ^ g))) . i = 1. (K,(f . i)) by A5, A11, FINSEQ_1:def 7
.= (1. (K,f)) . i by A13, Def8
.= ((1. (K,f)) ^ (1. (K,g))) . i by A13, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose ex n being Nat st
( n in dom (1. (K,g)) & i = (len (1. (K,f))) + n ) ; :: thesis: (1. (K,(f ^ g))) . i = ((1. (K,f)) ^ (1. (K,g))) . i

then consider n being Nat such that
A14: n in dom (1. (K,g)) and
A15: i = (len (1. (K,f))) + n ;
thus (1. (K,(f ^ g))) . i = 1. (K,(g . n)) by A3, A6, A11, A14, A15, FINSEQ_1:def 7
.= (1. (K,g)) . n by A14, Def8
.= ((1. (K,f)) ^ (1. (K,g))) . i by A14, A15, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence (1. (K,(f ^ g))) . i = ((1. (K,f)) ^ (1. (K,g))) . i ; :: thesis: verum

end;

len (1. (K,(f ^ g))) = len (f ^ g) by A2, FINSEQ_3:29;
hence 1. (K,(f ^ g)) = (1. (K,f)) ^ (1. (K,g)) by A6, A4, A1, A8, FINSEQ_1:14, FINSEQ_1:22; :: thesis: verum