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 . (e,d) = e holds

F [:] (([#] (p,e)),d) = [#] ((F [:] (p,d)),e)

let d, e 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)

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

hence
F [:] (([#] (p,e)),d) = [#] ((F [:] (p,d)),e)
by FUNCT_2:63; :: thesis: verumlet 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:84;

end;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:84;

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

hence
(F [:] (([#] (p,e)),d)) . i = ([#] ((F [:] (p,d)),e)) . i
by FUNCOP_1:48; :: thesis: verumper cases
( i in dom p or not i in dom p )
;

end;