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:35;
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:31;
A5: dom (1. K,f) = dom f by Def8;
then A6: len (1. K,f) = len f by FINSEQ_3:31;
A7: len ((1. K,f) ^ (1. K,g)) = (len (1. K,f)) + (len (1. K,g)) by FINSEQ_1:35;

A8: now

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:27;
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:27;

now

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:38;

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:31;
hence 1. K,(f ^ g) = (1. K,f) ^ (1. K,g) by A6, A4, A1, A8, FINSEQ_1:18, FINSEQ_1:35; :: thesis: verum