let D be set ; for Y being FinSequenceSet of D
for F1, F2 being FinSequence of Y holds Length (F1 ^ F2) = (Length F1) ^ (Length F2)
let Y be FinSequenceSet of D; for F1, F2 being FinSequence of Y holds Length (F1 ^ F2) = (Length F1) ^ (Length F2)
let F1, F2 be FinSequence of Y; Length (F1 ^ F2) = (Length F1) ^ (Length F2)
B1:
( dom (Length (F1 ^ F2)) = dom (F1 ^ F2) & dom (Length F1) = dom F1 & dom (Length F2) = dom F2 )
by Def1;
then A1:
( len (Length (F1 ^ F2)) = len (F1 ^ F2) & len (Length F1) = len F1 & len (Length F2) = len F2 )
by FINSEQ_3:29;
B2:
len ((Length F1) ^ (Length F2)) = (len (Length F1)) + (len (Length F2))
by FINSEQ_1:22;
then A2:
len (Length (F1 ^ F2)) = len ((Length F1) ^ (Length F2))
by A1, FINSEQ_1:22;
now for k being Nat st 1 <= k & k <= len (Length (F1 ^ F2)) holds
(Length (F1 ^ F2)) . k = ((Length F1) ^ (Length F2)) . klet k be
Nat;
( 1 <= k & k <= len (Length (F1 ^ F2)) implies (Length (F1 ^ F2)) . b1 = ((Length F1) ^ (Length F2)) . b1 )assume A3:
( 1
<= k &
k <= len (Length (F1 ^ F2)) )
;
(Length (F1 ^ F2)) . b1 = ((Length F1) ^ (Length F2)) . b1then
k in dom (Length (F1 ^ F2))
by FINSEQ_3:25;
then A4:
(Length (F1 ^ F2)) . k = len ((F1 ^ F2) . k)
by Def1;
per cases
( k <= len (Length F1) or len (Length F1) < k )
;
suppose A7:
len (Length F1) < k
;
(Length (F1 ^ F2)) . b1 = ((Length F1) ^ (Length F2)) . b1then
(len (Length F1)) + 1
<= k
by NAT_1:13;
then
k - ((len (Length F1)) + 1) is
Nat
by NAT_1:21;
then reconsider k1 =
(k - (len (Length F1))) - 1 as
Nat ;
k <= (len (Length F1)) + (len (Length F2))
by A3, A1, FINSEQ_1:22;
then
k - (len (Length F1)) <= len (Length F2)
by XREAL_1:20;
then A10:
k1 + 1
in dom (Length F2)
by FINSEQ_3:25, NAT_1:11;
((Length F1) ^ (Length F2)) . k =
(Length F2) . (k1 + 1)
by A2, A3, A7, FINSEQ_1:24
.=
len (F2 . (k1 + 1))
by A10, Def1
;
hence
(Length (F1 ^ F2)) . k = ((Length F1) ^ (Length F2)) . k
by A4, A3, A1, A7, FINSEQ_1:24;
verum end; end;
hence
Length (F1 ^ F2) = (Length F1) ^ (Length F2)
by B2, A1, FINSEQ_1:22; verum