let DK, DX be non empty set ; 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; 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; 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; ( fp = F * p & fq = F * q implies F * (p ^ q) = fp ^ fq )
assume A1:
( fp = F * p & fq = F * q )
; 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 ;
( x in dom (F * (p ^ q)) implies (fp ^ fq) . x = (F * (p ^ q)) . x )
assume A6:
x in dom (F * (p ^ q))
;
(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 A10:
not
n <= len p
;
(fp ^ fq) . x = (F * (p ^ q)) . xthen
(
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
;
verum end;
end;
hence
F * (p ^ q) = fp ^ fq
by A4, A5, FUNCT_1:2; verum