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

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

now

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 Th22
.= F . (p . i),(q . i) by A1, A5, A6, A7, Th22
.= (F .: p,q) . i by A3, A5, A4, A7, FUNCOP_1:28
.= ([#] (F .: p,q),e) . i by A3, A5, A4, A7, Th22 ;
:: 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 Th22
.= e by A1, A2, A5, A6, A8, Th22
.= ([#] (F .: p,q),e) . i by A3, A5, A4, A8, Th22 ;
:: thesis: verum

end;

end;

end;

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

end;

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