let f be Function; :: thesis: for p1, p2, f1, f2 being FinSequence st rng p1 c= dom f & rng p2 c= dom f & f1 = f * p1 & f2 = f * p2 holds
f * (p1 ^ p2) = f1 ^ f2
let p1, p2, f1, f2 be FinSequence; :: thesis: ( rng p1 c= dom f & rng p2 c= dom f & f1 = f * p1 & f2 = f * p2 implies f * (p1 ^ p2) = f1 ^ f2 )
assume that
A1: rng p1 c= dom f and
A2: rng p2 c= dom f and
A3: f1 = f * p1 and
A4: f2 = f * p2 ; :: thesis: f * (p1 ^ p2) = f1 ^ f2
A5: dom (p1 ^ p2) = Seg ((len p1) + (len p2)) by FINSEQ_1:def 7;
rng (p1 ^ p2) = (rng p1) \/ (rng p2) by FINSEQ_1:31;
then A6: dom (f * (p1 ^ p2)) = dom (p1 ^ p2) by A1, A2, RELAT_1:27, XBOOLE_1:8;
A7: dom f1 = dom p1 by A1, A3, RELAT_1:27;
then A8: len f1 = len p1 by FINSEQ_3:29;
A9: dom f2 = dom p2 by A2, A4, RELAT_1:27;
then len f2 = len p2 by FINSEQ_3:29;
then A10: dom (f1 ^ f2) = dom (f * (p1 ^ p2)) by A6, A8, A5, FINSEQ_1:def 7;

now :: thesis: for x being object st x in dom (f1 ^ f2) holds
(f1 ^ f2) . x = (f * (p1 ^ p2)) . x

let x be object ; :: thesis: ( x in dom (f1 ^ f2) implies (f1 ^ f2) . x = (f * (p1 ^ p2)) . x )
assume A11: x in dom (f1 ^ f2) ; :: thesis: (f1 ^ f2) . x = (f * (p1 ^ p2)) . x
reconsider i = x as Element of NAT by A11;

now :: thesis: (f1 ^ f2) . i = (f * (p1 ^ p2)) . i

per cases ( i in dom p1 or not i in dom p1 ) ;

suppose A12: i in dom p1 ; :: thesis: (f1 ^ f2) . i = (f * (p1 ^ p2)) . i

hence (f1 ^ f2) . i = f1 . i by A7, FINSEQ_1:def 7
.= f . (p1 . i) by A3, A7, A12, FUNCT_1:12
.= f . ((p1 ^ p2) . i) by A12, FINSEQ_1:def 7
.= (f * (p1 ^ p2)) . i by A10, A11, FUNCT_1:12 ;
:: thesis: verum

end;

suppose not i in dom p1 ; :: thesis: (f1 ^ f2) . i = (f * (p1 ^ p2)) . i

then consider n being Nat such that
A13: n in dom p2 and
A14: i = (len p1) + n by A7, A9, A8, A11, FINSEQ_1:25;
thus (f1 ^ f2) . i = f2 . n by A9, A8, A13, A14, FINSEQ_1:def 7
.= f . (p2 . n) by A4, A9, A13, FUNCT_1:12
.= f . ((p1 ^ p2) . i) by A13, A14, FINSEQ_1:def 7
.= (f * (p1 ^ p2)) . i by A10, A11, FUNCT_1:12 ; :: thesis: verum

end;

end;

end;

hence (f1 ^ f2) . x = (f * (p1 ^ p2)) . x ; :: thesis: verum

end;

hence f * (p1 ^ p2) = f1 ^ f2 by A10, FUNCT_1:2; :: thesis: verum