let W be non empty set ; :: thesis: for h1, h2 being PartFunc of W,REAL
for seq being sequence of W st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
let h1, h2 be PartFunc of W,REAL; :: thesis: for seq being sequence of W st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
let seq be sequence of W; :: thesis: ( rng seq c= (dom h1) /\ (dom h2) implies ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) )
A1: (dom h1) /\ (dom h2) c= dom h1 by XBOOLE_1:17;
A2: (dom h1) /\ (dom h2) c= dom h2 by XBOOLE_1:17;
assume A3: rng seq c= (dom h1) /\ (dom h2) ; :: thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
then A4: rng seq c= dom (h1 + h2) by VALUED_1:def 1;

now :: thesis: for n being Nat holds ((h1 + h2) /* seq) . n = ((h1 /* seq) . n) + ((h2 /* seq) . n)

let n be Nat; :: thesis: ((h1 + h2) /* seq) . n = ((h1 /* seq) . n) + ((h2 /* seq) . n)
A5: n in NAT by ORDINAL1:def 12;
A6: seq . n in rng seq by VALUED_0:28;
thus ((h1 + h2) /* seq) . n = (h1 + h2) . (seq . n) by A4, FUNCT_2:108, A5
.= (h1 . (seq . n)) + (h2 . (seq . n)) by A4, A6, VALUED_1:def 1
.= ((h1 /* seq) . n) + (h2 . (seq . n)) by A3, A1, FUNCT_2:108, XBOOLE_1:1, A5
.= ((h1 /* seq) . n) + ((h2 /* seq) . n) by A3, A2, FUNCT_2:108, XBOOLE_1:1, A5 ; :: thesis: verum

end;

hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by SEQ_1:7; :: thesis: ( (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
A7: rng seq c= dom (h1 - h2) by A3, VALUED_1:12;

now :: thesis: for n being Nat holds ((h1 - h2) /* seq) . n = ((h1 /* seq) . n) - ((h2 /* seq) . n)

let n be Nat; :: thesis: ((h1 - h2) /* seq) . n = ((h1 /* seq) . n) - ((h2 /* seq) . n)
A8: n in NAT by ORDINAL1:def 12;
A9: seq . n in rng seq by VALUED_0:28;
thus ((h1 - h2) /* seq) . n = (h1 - h2) . (seq . n) by A7, FUNCT_2:108, A8
.= (h1 . (seq . n)) - (h2 . (seq . n)) by A7, A9, VALUED_1:13
.= ((h1 /* seq) . n) - (h2 . (seq . n)) by A3, A1, FUNCT_2:108, XBOOLE_1:1, A8
.= ((h1 /* seq) . n) - ((h2 /* seq) . n) by A3, A2, FUNCT_2:108, XBOOLE_1:1, A8 ; :: thesis: verum

end;

hence (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by Th1; :: thesis: (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq)
A10: rng seq c= dom (h1 (#) h2) by A3, VALUED_1:def 4;

now :: thesis: for n being Nat holds ((h1 (#) h2) /* seq) . n = ((h1 /* seq) . n) * ((h2 /* seq) . n)

let n be Nat; :: thesis: ((h1 (#) h2) /* seq) . n = ((h1 /* seq) . n) * ((h2 /* seq) . n)
A11: n in NAT by ORDINAL1:def 12;
thus ((h1 (#) h2) /* seq) . n = (h1 (#) h2) . (seq . n) by A10, FUNCT_2:108, A11
.= (h1 . (seq . n)) * (h2 . (seq . n)) by VALUED_1:5
.= ((h1 /* seq) . n) * (h2 . (seq . n)) by A3, A1, FUNCT_2:108, XBOOLE_1:1, A11
.= ((h1 /* seq) . n) * ((h2 /* seq) . n) by A3, A2, FUNCT_2:108, XBOOLE_1:1, A11 ; :: thesis: verum

end;

hence (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) by SEQ_1:8; :: thesis: verum