let D be non empty set ; 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; 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; 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; ( 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
; 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 for i being Element of NAT holds (F .: (([#] (p,e)),([#] (q,e)))) . i = ([#] ((F .: (p,q)),e)) . ilet i be
Element of
NAT ;
(F .: (([#] (p,e)),([#] (q,e)))) . i = ([#] ((F .: (p,q)),e)) . inow F . ((([#] (p,e)) . i),(([#] (q,e)) . i)) = ([#] ((F .: (p,q)),e)) . iper cases
( i in dom p or not i in dom p )
;
suppose A7:
i in dom p
;
F . ((([#] (p,e)) . i),(([#] (q,e)) . i)) = ([#] ((F .: (p,q)),e)) . ihence 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
;
verum end; suppose A8:
not
i in dom p
;
F . ((([#] (p,e)) . i),(([#] (q,e)) . i)) = ([#] ((F .: (p,q)),e)) . ihence 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
;
verum end; end; end; hence
(F .: (([#] (p,e)),([#] (q,e)))) . i = ([#] ((F .: (p,q)),e)) . i
by FUNCOP_1:37;
verum end;
hence
F .: (([#] (p,e)),([#] (q,e))) = [#] ((F .: (p,q)),e)
by FUNCT_2:63; verum