let D be non empty set ; :: thesis: for H1, H2 being Functional_Sequence of D,REAL
for x being Element of D st {x} common_on_dom H1 & {x} common_on_dom H2 holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x )
let H1, H2 be Functional_Sequence of D,REAL ; :: thesis: for x being Element of D st {x} common_on_dom H1 & {x} common_on_dom H2 holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x )
let x be Element of D; :: thesis: ( {x} common_on_dom H1 & {x} common_on_dom H2 implies ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) )
assume A1: ( {x} common_on_dom H1 & {x} common_on_dom H2 ) ; :: thesis: ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x )

now

let n be Element of NAT ; :: thesis: ((H1 # x) + (H2 # x)) . n = ((H1 + H2) # x) . n
A2: x in {x} by TARSKI:def 1;
( {x} c= dom (H1 . n) & {x} c= dom (H2 . n) ) by A1, Def10;
then x in (dom (H1 . n)) /\ (dom (H2 . n)) by A2, XBOOLE_0:def 4;
then A3: x in dom ((H1 . n) + (H2 . n)) by VALUED_1:def 1;
thus ((H1 # x) + (H2 # x)) . n = ((H1 # x) . n) + ((H2 # x) . n) by SEQ_1:11
.= ((H1 . n) . x) + ((H2 # x) . n) by Def11
.= ((H1 . n) . x) + ((H2 . n) . x) by Def11
.= ((H1 . n) + (H2 . n)) . x by A3, VALUED_1:def 1
.= ((H1 + H2) . n) . x by Def6
.= ((H1 + H2) # x) . n by Def11 ; :: thesis: verum

end;

hence (H1 # x) + (H2 # x) = (H1 + H2) # x by FUNCT_2:113; :: thesis: ( (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x )

now

let n be Element of NAT ; :: thesis: ((H1 # x) - (H2 # x)) . n = ((H1 - H2) # x) . n
A4: x in {x} by TARSKI:def 1;
( {x} c= dom (H1 . n) & {x} c= dom (H2 . n) ) by A1, Def10;
then x in (dom (H1 . n)) /\ (dom (H2 . n)) by A4, XBOOLE_0:def 4;
then A5: x in dom ((H1 . n) - (H2 . n)) by VALUED_1:12;
thus ((H1 # x) - (H2 # x)) . n = ((H1 # x) . n) - ((H2 # x) . n) by RFUNCT_2:6
.= ((H1 . n) . x) - ((H2 # x) . n) by Def11
.= ((H1 . n) . x) - ((H2 . n) . x) by Def11
.= ((H1 . n) - (H2 . n)) . x by A5, VALUED_1:13
.= ((H1 - H2) . n) . x by Th4
.= ((H1 - H2) # x) . n by Def11 ; :: thesis: verum

end;

hence (H1 # x) - (H2 # x) = (H1 - H2) # x by FUNCT_2:113; :: thesis: (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x

now

let n be Element of NAT ; :: thesis: ((H1 # x) (#) (H2 # x)) . n = ((H1 (#) H2) # x) . n
thus ((H1 # x) (#) (H2 # x)) . n = ((H1 # x) . n) * ((H2 # x) . n) by SEQ_1:12
.= ((H1 . n) . x) * ((H2 # x) . n) by Def11
.= ((H1 . n) . x) * ((H2 . n) . x) by Def11
.= ((H1 . n) (#) (H2 . n)) . x by VALUED_1:5
.= ((H1 (#) H2) . n) . x by Def8
.= ((H1 (#) H2) # x) . n by Def11 ; :: thesis: verum

end;

hence (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x by FUNCT_2:113; :: thesis: verum