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;
C2: rng (p ^ q) = (rng p) \/ (rng q) by AFINSQ_1:29;
then A2: dom (f * (p ^ q)) = dom (p ^ q) by RELAT_1:46, A1, XBOOLE_1:8;
reconsider fpq = f * (p ^ q) as XFinSequence by C2, A1, XBOOLE_1:8, AFINSQ_1:13;
A3: ( dom fp = dom p & dom fq = dom q ) by A1, RELAT_1:46;
A4: ( dom (p ^ q) = (len p) + (len q) & dom (fp ^ fq) = (len fp) + (len fq) ) by AFINSQ_1:def 4;
A5: len fpq = len (fp ^ fq) by C2, RELAT_1:46, A1, XBOOLE_1:8, A3, A4;
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 G1: k < len fpq ; :: thesis: (fp ^ fq) . k = fpq . k
then G2: k in dom fpq by NAT_1:45;

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 NAT_1:45;
then ( (p ^ q) . k = p . k & fp . k = f . (p . k) & (fp ^ fq) . k = fp . k ) by A1, A3, AFINSQ_1:def 4, FUNCT_1:23;
hence (fp ^ fq) . k = fpq . k by G2, FUNCT_1:22; :: thesis: verum

end;

suppose G3: 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 A4, C2, RELAT_1:46, A1, XBOOLE_1:8, G1;
then kp < len q by XREAL_1:9;
then kp in dom q by NAT_1:45;
then ( (p ^ q) . k = q . kp & (fp ^ fq) . k = fq . kp & fq . kp = f . (q . kp) ) by AFINSQ_1:21, G1, A1, A2, A3, A4, G3, FUNCT_1:23;
hence (fp ^ fq) . k = fpq . k by G2, FUNCT_1:22; :: thesis: verum

end;

end;

end;

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