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

now

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

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

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