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 A1: ( fp = F * p & fq = F * q ) ; :: thesis: F * (p ^ q) = fp ^ fq
then A2: ( dom fp = dom p & dom fq = dom q ) by FINSEQ_3:120;
A3: ( len fp = len p & len fq = len q ) by A1, FINSEQ_3:120;
then A4: dom (fp ^ fq) = Seg ((len p) + (len q)) by FINSEQ_1:def 7;
A5: dom (F * (p ^ q)) = dom (p ^ q) by FINSEQ_3:120
.= Seg ((len p) + (len q)) by FINSEQ_1:def 7 ;
for x being object st x in dom (F * (p ^ q)) holds
(fp ^ fq) . x = (F * (p ^ q)) . x

proof

let x be object ; :: thesis: ( x in dom (F * (p ^ q)) implies (fp ^ fq) . x = (F * (p ^ q)) . x )
assume A6: x in dom (F * (p ^ q)) ; :: thesis: (fp ^ fq) . x = (F * (p ^ q)) . x
then reconsider n = x as Element of NAT ;
A7: ( 1 <= n & n <= (len p) + (len q) ) by A6, A5, FINSEQ_1:1;
A8: (F * (p ^ q)) . n = F . ((p ^ q) . n) by A6, FINSEQ_3:120;

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 A7;
then A9: n in dom p by FINSEQ_1:def 3;
hence (F * (p ^ q)) . x = F . (p . n) by A8, FINSEQ_1:def 7
.= fp . n by A1, A9, A2, FINSEQ_3:120
.= (fp ^ fq) . x by A9, A2, FINSEQ_1:def 7 ;
:: thesis: verum

end;

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

then ( len p < n & n <= len (p ^ q) ) by A7, FINSEQ_1:22;
then A11: (p ^ q) . n = q . (n - (len p)) by FINSEQ_1:24;
A12: n - (len p) <= ((len p) + (len q)) - (len p) by A7, XREAL_1:9;
A13: (len p) - (len p) < n - (len p) by A10, XREAL_1:9;
A14: n - (len p) is Element of NAT by A13, INT_1:3;
then 1 <= n - (len p) by A13, NAT_1:14;
then n - (len p) in Seg (len q) by A12, A14;
then A15: n - (len p) in dom q by FINSEQ_1:def 3;
A16: ( len fp < n & n <= len (fp ^ fq) ) by A3, A10, A7, FINSEQ_1:22;
thus (F * (p ^ q)) . x = fq . (n - (len p)) by A1, A15, A2, A11, A8, FINSEQ_3:120
.= (fp ^ fq) . x by A16, A3, FINSEQ_1:24 ; :: thesis: verum

end;

end;

end;

hence F * (p ^ q) = fp ^ fq by A4, A5, FUNCT_1:2; :: thesis: verum