let K be Field; 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 ; 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 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))) . ilet i be
Nat;
( 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)))
;
(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 (1. (K,(f ^ g))) . i = ((1. (K,f)) ^ (1. (K,g))) . iper 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
ex
n being
Nat st
(
n in dom (1. (K,g)) &
i = (len (1. (K,f))) + n )
;
(1. (K,(f ^ g))) . i = ((1. (K,f)) ^ (1. (K,g))) . ithen 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
;
verum end; end; end; hence
(1. (K,(f ^ g))) . i = ((1. (K,f)) ^ (1. (K,g))) . i
;
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; verum