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

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 A3: ( 1 <= i & i <= len ((1. K,f) ^ (1. K,g)) ) ; :: thesis: (1. K,(f ^ g)) . i = ((1. K,f) ^ (1. K,g)) . i
A4: ( i in dom ((1. K,f) ^ (1. K,g)) & i in dom (1. K,(f ^ g)) ) by A2, A3, FINSEQ_3:27;
then A5: (1. K,(f ^ g)) . i = 1. K,((f ^ g) . i) by Def8;

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 A4, FINSEQ_1:38;

suppose A6: 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 A1, A5, FINSEQ_1:def 7
.= (1. K,f) . i by A6, Def8
.= ((1. K,f) ^ (1. K,g)) . i by A6, 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
A7: ( n in dom (1. K,g) & i = (len (1. K,f)) + n ) ;
thus (1. K,(f ^ g)) . i = 1. K,(g . n) by A1, A2, A5, A7, FINSEQ_1:def 7
.= (1. K,g) . n by A7, Def8
.= ((1. K,f) ^ (1. K,g)) . i by A7, 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;

hence 1. K,(f ^ g) = (1. K,f) ^ (1. K,g) by A2, FINSEQ_1:18; :: thesis: verum