let D be non empty set ; :: thesis: for e, d being Element of D
for F being BinOp of D
for p being FinSequence of D st F . (e,d) = e holds
F [:] (([#] (p,e)),d) = [#] ((F [:] (p,d)),e)
let e, d be Element of D; :: thesis: for F being BinOp of D
for p being FinSequence of D st F . (e,d) = e holds
F [:] (([#] (p,e)),d) = [#] ((F [:] (p,d)),e)
let F be BinOp of D; :: thesis: for p being FinSequence of D st F . (e,d) = e holds
F [:] (([#] (p,e)),d) = [#] ((F [:] (p,d)),e)
let p be FinSequence of D; :: thesis: ( F . (e,d) = e implies F [:] (([#] (p,e)),d) = [#] ((F [:] (p,d)),e) )
assume A1: F . (e,d) = e ; :: thesis: F [:] (([#] (p,e)),d) = [#] ((F [:] (p,d)),e)

now

let i be Element of NAT ; :: thesis: (F [:] (([#] (p,e)),d)) . i = ([#] ((F [:] (p,d)),e)) . i
A2: dom p = Seg (len p) by FINSEQ_1:def 3;
A3: ( len (F [:] (p,d)) = len p & dom (F [:] (p,d)) = Seg (len (F [:] (p,d))) ) by FINSEQ_1:def 3, FINSEQ_2:98;

now

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

suppose A4: i in dom p ; :: thesis: F . ((([#] (p,e)) . i),d) = ([#] ((F [:] (p,d)),e)) . i

hence F . ((([#] (p,e)) . i),d) = F . ((p . i),d) by Th22
.= (F [:] (p,d)) . i by A3, A2, A4, FUNCOP_1:35
.= ([#] ((F [:] (p,d)),e)) . i by A3, A2, A4, Th22 ;
:: thesis: verum

end;

suppose A5: not i in dom p ; :: thesis: F . ((([#] (p,e)) . i),d) = ([#] ((F [:] (p,d)),e)) . i

hence F . ((([#] (p,e)) . i),d) = F . (e,d) by Th22
.= ([#] ((F [:] (p,d)),e)) . i by A1, A3, A2, A5, Th22 ;
:: thesis: verum

end;

end;

end;

hence (F [:] (([#] (p,e)),d)) . i = ([#] ((F [:] (p,d)),e)) . i by FUNCOP_1:60; :: thesis: verum

end;

hence F [:] (([#] (p,e)),d) = [#] ((F [:] (p,d)),e) by FUNCT_2:113; :: thesis: verum