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 :: thesis: for i being Element of NAT holds (F [;] (d,([#] (p,e)))) . i = ([#] ((F [;] (d,p)),e)) . i

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:78;

now :: thesis: F . (d,(([#] (p,e)) . i)) = ([#] ((F [;] (d,p)),e)) . i

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 Th20
.= (F [;] (d,p)) . i by A3, A2, A4, FUNCOP_1:32
.= ([#] ((F [;] (d,p)),e)) . i by A3, A2, A4, Th20 ;
:: 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 Th20
.= ([#] ((F [;] (d,p)),e)) . i by A1, A3, A2, A5, Th20 ;
:: thesis: verum

end;

end;

end;

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

end;

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