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)
A1: f = (p ^ <*f*>) . ((len p) + 1) by FINSEQ_1:59;
len <*f*> = 1 by FINSEQ_1:57;
then A2: len (p ^ <*f*>) = (len p) + 1 by FINSEQ_1:35;
consider ff being ManySortedFunction of NAT such that
A3: compose (p ^ <*f*>),X = ff . (len (p ^ <*f*>)) and
A4: ff . 0 = id X and
A5: 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;
reconsider g = ff . (len p) as Function ;
A6: dom p c= dom (p ^ <*f*>) by FINSEQ_1:39;

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 A7: 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 that
A8: g = ff . i and
A9: h = p . (i + 1) ; :: thesis: ff . (i + 1) = h * g
h = (p ^ <*f*>) . (i + 1) by A7, A9, FINSEQ_1:def 7;
hence ff . (i + 1) = h * g by A5, A6, A7, A8; :: thesis: verum

end;

then A10: g = compose p,X by A4, Def4;
( 1 in Seg 1 & dom <*f*> = Seg 1 ) by FINSEQ_1:4, FINSEQ_1:55, TARSKI:def 1;
hence compose (p ^ <*f*>),X = f * (compose p,X) by A3, A5, A10, A2, A1, FINSEQ_1:41; :: thesis: verum