let DK, DX be non empty set ; :: thesis: for F being Function of DX,DK
for p, q being FinSequence of DX
for fp, fq being FinSequence of DK st fp = F * p & fq = F * q holds
F * (p ^ q) = fp ^ fq
let F be Function of DX,DK; :: thesis: for p, q being FinSequence of DX
for fp, fq being FinSequence of DK st fp = F * p & fq = F * q holds
F * (p ^ q) = fp ^ fq
let p, q be FinSequence of DX; :: thesis: for fp, fq being FinSequence of DK st fp = F * p & fq = F * q holds
F * (p ^ q) = fp ^ fq
let fp, fq be FinSequence of DK; :: thesis: ( fp = F * p & fq = F * q implies F * (p ^ q) = fp ^ fq )
assume AS: ( fp = F * p & fq = F * q ) ; :: thesis: F * (p ^ q) = fp ^ fq
then P0: ( dom fp = dom p & dom fq = dom q ) by FINSEQ_3:129;
P1: ( len fp = len p & len fq = len q ) by FINSEQ_3:129, AS;
then P2: dom (fp ^ fq) = Seg ((len p) + (len q)) by FINSEQ_1:def 7;
P3: dom (F * (p ^ q)) = dom (p ^ q) by FINSEQ_3:129
.= Seg ((len p) + (len q)) by FINSEQ_1:def 7 ;
for x being set st x in dom (F * (p ^ q)) holds
(fp ^ fq) . x = (F * (p ^ q)) . x

proof

let x be set ; :: thesis: ( x in dom (F * (p ^ q)) implies (fp ^ fq) . x = (F * (p ^ q)) . x )
assume A1: x in dom (F * (p ^ q)) ; :: thesis: (fp ^ fq) . x = (F * (p ^ q)) . x
then reconsider n = x as Element of NAT ;
A4: ( 1 <= n & n <= (len p) + (len q) ) by A1, P3, FINSEQ_1:3;
A2: (F * (p ^ q)) . n = F . ((p ^ q) . n) by A1, FINSEQ_3:129;

per cases ( n <= len p or not n <= len p ) ;

suppose n <= len p ; :: thesis: (fp ^ fq) . x = (F * (p ^ q)) . x

then n in Seg (len p) by A4;
then A22: n in dom p by FINSEQ_1:def 3;
hence (F * (p ^ q)) . x = F . (p . n) by FINSEQ_1:def 7, A2
.= fp . n by AS, A22, P0, FINSEQ_3:129
.= (fp ^ fq) . x by A22, P0, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose A23: not n <= len p ; :: thesis: (fp ^ fq) . x = (F * (p ^ q)) . x

then ( len p < n & n <= len (p ^ q) ) by A4, FINSEQ_1:35;
then A24: (p ^ q) . n = q . (n - (len p)) by FINSEQ_1:37;
A241: n - (len p) <= ((len p) + (len q)) - (len p) by XREAL_1:11, A4;
A242: (len p) - (len p) < n - (len p) by A23, XREAL_1:11;
then A243: n - (len p) is Element of NAT by INT_1:16;
then 1 <= n - (len p) by A242, NAT_1:14;
then n - (len p) in Seg (len q) by A241, A243;
then A25: n - (len p) in dom q by FINSEQ_1:def 3;
A26: ( len fp < n & n <= len (fp ^ fq) ) by P1, A23, FINSEQ_1:35, A4;
thus (F * (p ^ q)) . x = fq . (n - (len p)) by AS, A25, P0, FINSEQ_3:129, A24, A2
.= (fp ^ fq) . x by A26, P1, FINSEQ_1:37 ; :: thesis: verum

end;

end;

end;

hence F * (p ^ q) = fp ^ fq by P2, P3, FUNCT_1:9; :: thesis: verum