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