let F, G be FinSequence-yielding FinSequence; :: thesis: for f, g being FinSequence st f in doms F & g in doms G holds
(App (F ^ G)) . (f ^ g) = ((App F) . f) ^ ((App G) . g)
let f, g be FinSequence; :: thesis: ( f in doms F & g in doms G implies (App (F ^ G)) . (f ^ g) = ((App F) . f) ^ ((App G) . g) )
set FG = F ^ G;
set AF = App F;
set AG = App G;
set AFG = App (F ^ G);
assume A1: ( f in doms F & g in doms G ) ; :: thesis: (App (F ^ G)) . (f ^ g) = ((App F) . f) ^ ((App G) . g)
then A2: f ^ g in doms (F ^ G) by Th48;
A3: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
then A4: ( len ((App F) . f) = len f & len ((App G) . g) = len g & len ((App (F ^ G)) . (f ^ g)) = (len f) + (len g) ) by A1, A2, Def9;
A5: ( len f = len F & len g = len G ) by A1, Th47;
then A6: ( dom f = dom F & dom g = dom G ) by FINSEQ_3:30;
for i being Nat st 1 <= i & i <= len ((App (F ^ G)) . (f ^ g)) holds
((App (F ^ G)) . (f ^ g)) . i = (((App F) . f) ^ ((App G) . g)) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len ((App (F ^ G)) . (f ^ g)) implies ((App (F ^ G)) . (f ^ g)) . i = (((App F) . f) ^ ((App G) . g)) . i )
assume ( 1 <= i & i <= len ((App (F ^ G)) . (f ^ g)) ) ; :: thesis: ((App (F ^ G)) . (f ^ g)) . i = (((App F) . f) ^ ((App G) . g)) . i
then A7: i in dom (f ^ g) by A3, A4, FINSEQ_3:25;

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

suppose A8: i in dom f ; :: thesis: ((App (F ^ G)) . (f ^ g)) . i = (((App F) . f) ^ ((App G) . g)) . i

then i in dom ((App F) . f) by A4, FINSEQ_3:29;
hence (((App F) . f) ^ ((App G) . g)) . i = ((App F) . f) . i by FINSEQ_1:def 7
.= (F . i) . (f . i) by A8, A1, Def9
.= ((F ^ G) . i) . (f . i) by A8, A6, FINSEQ_1:def 7
.= ((F ^ G) . i) . ((f ^ g) . i) by A8, FINSEQ_1:def 7
.= ((App (F ^ G)) . (f ^ g)) . i by A2, A7, Def9 ;
:: thesis: verum

end;

suppose ex n being Nat st
( n in dom g & i = (len f) + n ) ; :: thesis: ((App (F ^ G)) . (f ^ g)) . i = (((App F) . f) ^ ((App G) . g)) . i

then consider n being Nat such that
A9: ( n in dom g & i = (len f) + n ) ;
n in dom ((App G) . g) by A4, A9, FINSEQ_3:29;
hence (((App F) . f) ^ ((App G) . g)) . i = ((App G) . g) . n by FINSEQ_1:def 7, A9, A4
.= (G . n) . (g . n) by A9, A1, Def9
.= ((F ^ G) . i) . (g . n) by A9, A5, A6, FINSEQ_1:def 7
.= ((F ^ G) . i) . ((f ^ g) . i) by A9, FINSEQ_1:def 7
.= ((App (F ^ G)) . (f ^ g)) . i by A2, A7, Def9 ;
:: thesis: verum

end;

end;

end;

hence (App (F ^ G)) . (f ^ g) = ((App F) . f) ^ ((App G) . g) by A4, FINSEQ_1:22; :: thesis: verum