let D be non empty set ; :: thesis: for e being Element of D
for F being BinOp of D
for p, q being FinSequence of D st len p = len q & F . (e,e) = e holds
F .: (([#] (p,e)),([#] (q,e))) = [#] ((F .: (p,q)),e)
let e be Element of D; :: thesis: for F being BinOp of D
for p, q being FinSequence of D st len p = len q & F . (e,e) = e holds
F .: (([#] (p,e)),([#] (q,e))) = [#] ((F .: (p,q)),e)
let F be BinOp of D; :: thesis: for p, q being FinSequence of D st len p = len q & F . (e,e) = e holds
F .: (([#] (p,e)),([#] (q,e))) = [#] ((F .: (p,q)),e)
let p, q be FinSequence of D; :: thesis: ( len p = len q & F . (e,e) = e implies F .: (([#] (p,e)),([#] (q,e))) = [#] ((F .: (p,q)),e) )
assume that
A1: len p = len q and
A2: F . (e,e) = e ; :: thesis: F .: (([#] (p,e)),([#] (q,e))) = [#] ((F .: (p,q)),e)
set r = F .: (p,q);
A3: len (F .: (p,q)) = len p by A1, FINSEQ_2:72;
A4: dom (F .: (p,q)) = Seg (len (F .: (p,q))) by FINSEQ_1:def 3;
A5: dom p = Seg (len p) by FINSEQ_1:def 3;
A6: dom q = Seg (len q) by FINSEQ_1:def 3;

now :: thesis: for i being Element of NAT holds (F .: (([#] (p,e)),([#] (q,e)))) . i = ([#] ((F .: (p,q)),e)) . i

let i be Element of NAT ; :: thesis: (F .: (([#] (p,e)),([#] (q,e)))) . i = ([#] ((F .: (p,q)),e)) . i

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

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

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

hence F . ((([#] (p,e)) . i),(([#] (q,e)) . i)) = F . ((p . i),(([#] (q,e)) . i)) by Th20
.= F . ((p . i),(q . i)) by A1, A5, A6, A7, Th20
.= (F .: (p,q)) . i by A3, A5, A4, A7, FUNCOP_1:22
.= ([#] ((F .: (p,q)),e)) . i by A3, A5, A4, A7, Th20 ;
:: thesis: verum

end;

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

hence F . ((([#] (p,e)) . i),(([#] (q,e)) . i)) = F . (e,(([#] (q,e)) . i)) by Th20
.= e by A1, A2, A5, A6, A8, Th20
.= ([#] ((F .: (p,q)),e)) . i by A3, A5, A4, A8, Th20 ;
:: thesis: verum

end;

end;

end;

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

end;

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