let X be set ; :: thesis: for p being Function-yielding FinSequence
for f being Function holds compose (p ^ <*f*>),X = f * (compose p,X)
let p be Function-yielding FinSequence; :: thesis: for f being Function holds compose (p ^ <*f*>),X = f * (compose p,X)
let f be Function; :: thesis: compose (p ^ <*f*>),X = f * (compose p,X)
consider ff being ManySortedFunction of NAT such that
A1: ( compose (p ^ <*f*>),X = ff . (len (p ^ <*f*>)) & ff . 0 = id X ) and
A2: for i being Element of NAT st i + 1 in dom (p ^ <*f*>) holds
for g, h being Function st g = ff . i & h = (p ^ <*f*>) . (i + 1) holds
ff . (i + 1) = h * g by Def4;
A3: dom p c= dom (p ^ <*f*>) by FINSEQ_1:39;
reconsider g = ff . (len p) as Function ;

now

let i be Element of NAT ; :: thesis: ( i + 1 in dom p implies for g, h being Function st g = ff . i & h = p . (i + 1) holds
ff . (i + 1) = h * g )
assume A4: i + 1 in dom p ; :: thesis: for g, h being Function st g = ff . i & h = p . (i + 1) holds
ff . (i + 1) = h * g
let g, h be Function; :: thesis: ( g = ff . i & h = p . (i + 1) implies ff . (i + 1) = h * g )
assume A5: ( g = ff . i & h = p . (i + 1) ) ; :: thesis: ff . (i + 1) = h * g
then h = (p ^ <*f*>) . (i + 1) by A4, FINSEQ_1:def 7;
hence ff . (i + 1) = h * g by A2, A3, A4, A5; :: thesis: verum

end;

then A6: g = compose p,X by A1, Def4;
( len <*f*> = 1 & 1 in Seg 1 & dom <*f*> = Seg 1 ) by FINSEQ_1:4, FINSEQ_1:55, FINSEQ_1:57, TARSKI:def 1;
then ( len (p ^ <*f*>) = (len p) + 1 & (len p) + 1 in dom (p ^ <*f*>) & f = (p ^ <*f*>) . ((len p) + 1) ) by FINSEQ_1:35, FINSEQ_1:41, FINSEQ_1:59;
hence compose (p ^ <*f*>),X = f * (compose p,X) by A1, A2, A6; :: thesis: verum