let f be Function; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: ( k < len fpq implies (fp ^ fq) . k = fpq . k )
assume A7: k < len fpq ; :: thesis: (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 k < len p ; :: thesis: (fp ^ fq) . k = fpq . k

then k in dom p by AFINSQ_1:86;
then ( (p ^ q) . k = p . k & fp . k = f . (p . k) & (fp ^ fq) . k = fp . k ) by A1, A4, AFINSQ_1:def 3, FUNCT_1:13;
hence (fp ^ fq) . k = fpq . k by A8, FUNCT_1:12; :: thesis: verum

end;

suppose A9: k >= len p ; :: thesis: (fp ^ fq) . k = fpq . k

then 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; :: thesis: verum

end;

end;

end;

hence fp ^ fq = f * (p ^ q) by A6, AFINSQ_1:9; :: thesis: verum