let f be Function; for p, q, fp, fq being XFinSequence st rng p c= dom f & rng q c= dom f & fp = f * p & fq = f * q holds
fp ^ fq = f * (p ^ q)
let p, q, fp, fq be XFinSequence; ( rng p c= dom f & rng q c= dom f & fp = f * p & fq = f * q implies fp ^ fq = f * (p ^ q) )
assume A1:
( rng p c= dom f & rng q c= dom f & fp = f * p & fq = f * q )
; fp ^ fq = f * (p ^ q)
set pq = p ^ q;
A2:
rng (p ^ q) = (rng p) \/ (rng q)
by AFINSQ_1:26;
then A3:
dom (f * (p ^ q)) = dom (p ^ q)
by A1, RELAT_1:27, XBOOLE_1:8;
reconsider fpq = f * (p ^ q) as XFinSequence by A2, A1, AFINSQ_1:10, XBOOLE_1:8;
A4:
( dom fp = dom p & dom fq = dom q )
by A1, RELAT_1:27;
A5:
( dom (p ^ q) = (len p) + (len q) & dom (fp ^ fq) = (len fp) + (len fq) )
by AFINSQ_1:def 3;
A6:
len fpq = len (fp ^ fq)
by A2, A1, A4, A5, RELAT_1:27, XBOOLE_1:8;
for k being Nat st k < len fpq holds
(fp ^ fq) . k = fpq . k
proof
let k be
Nat;
( k < len fpq implies (fp ^ fq) . k = fpq . k )
assume A7:
k < len fpq
;
(fp ^ fq) . k = fpq . k
then A8:
k in dom fpq
by AFINSQ_1:86;
per cases
( k < len p or k >= len p )
;
suppose A9:
k >= len p
;
(fp ^ fq) . k = fpq . kthen reconsider kp =
k - (len p) as
Element of
NAT by NAT_1:21;
(len p) + kp < (len p) + (len q)
by A5, A2, A1, A7, RELAT_1:27, XBOOLE_1:8;
then
kp < len q
by XREAL_1:7;
then
(
(p ^ q) . k = q . kp &
(fp ^ fq) . k = fq . kp &
fq . kp = f . (q . kp) )
by A7, A1, A3, A4, A5, A9, AFINSQ_1:18, FUNCT_1:13, AFINSQ_1:86;
hence
(fp ^ fq) . k = fpq . k
by A8, FUNCT_1:12;
verum end;
end;
hence
fp ^ fq = f * (p ^ q)
by A6, AFINSQ_1:9; verum