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 ;
A7: dom f1 = dom p1 by ;
then A8: len f1 = len p1 by FINSEQ_3:29;
A9: dom f2 = dom p2 by ;
then len f2 = len p2 by FINSEQ_3:29;
then A10: dom (f1 ^ f2) = dom (f * (p1 ^ p2)) by ;
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
.= f . (p1 . i) by
.= f . ((p1 ^ p2) . i) by
.= (f * (p1 ^ p2)) . i by ;
:: 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 ;
thus (f1 ^ f2) . i = f2 . n by
.= f . (p2 . n) by
.= f . ((p1 ^ p2) . i) by
.= (f * (p1 ^ p2)) . i by ; :: thesis: verum
end;
end;
end;
hence (f1 ^ f2) . x = (f * (p1 ^ p2)) . x ; :: thesis: verum
end;
hence f * (p1 ^ p2) = f1 ^ f2 by ; :: thesis: verum