let seq be Complex_Sequence; :: thesis: for h1, h2 being PartFunc of COMPLEX ,COMPLEX 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 COMPLEX ,COMPLEX ; :: 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) ) )
assume A1: 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) )
A2: ( (dom h1) /\ (dom h2) c= dom h1 & (dom h1) /\ (dom h2) c= dom h2 ) by XBOOLE_1:17;
A3: rng seq c= dom (h1 + h2) by A1, VALUED_1:def 1;
A4: rng seq c= dom (h1 - h2) by A1, CFUNCT_1:4;
A5: rng seq c= dom (h1 (#) h2) by A1, VALUED_1:def 4;

now

let n be Element of NAT ; :: thesis: ((h1 + h2) /* seq) . n = ((h1 /* seq) + (h2 /* seq)) . n
seq . n in rng seq by VALUED_0:28;
then A6: seq . n in dom (h1 + h2) by A3;
thus ((h1 + h2) /* seq) . n = (h1 + h2) /. (seq . n) by A3, FUNCT_2:186
.= (h1 /. (seq . n)) + (h2 /. (seq . n)) by A6, CFUNCT_1:3
.= ((h1 /* seq) . n) + (h2 /. (seq . n)) by A1, A2, FUNCT_2:186, XBOOLE_1:1
.= ((h1 /* seq) . n) + ((h2 /* seq) . n) by A1, A2, FUNCT_2:186, XBOOLE_1:1
.= ((h1 /* seq) + (h2 /* seq)) . n by VALUED_1:1 ; :: thesis: verum

end;

hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by FUNCT_2:113; :: thesis: ( (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )

now

let n be Element of NAT ; :: thesis: ((h1 - h2) /* seq) . n = ((h1 /* seq) . n) - ((h2 /* seq) . n)
seq . n in rng seq by VALUED_0:28;
then A7: seq . n in dom (h1 - h2) by A4;
thus ((h1 - h2) /* seq) . n = (h1 - h2) /. (seq . n) by A4, FUNCT_2:186
.= (h1 /. (seq . n)) - (h2 /. (seq . n)) by A7, CFUNCT_1:4
.= ((h1 /* seq) . n) - (h2 /. (seq . n)) by A1, A2, FUNCT_2:186, XBOOLE_1:1
.= ((h1 /* seq) . n) - ((h2 /* seq) . n) by A1, A2, FUNCT_2:186, XBOOLE_1:1 ; :: thesis: verum

end;

hence (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by Th2; :: thesis: (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq)

now

let n be Element of NAT ; :: thesis: ((h1 (#) h2) /* seq) . n = ((h1 /* seq) (#) (h2 /* seq)) . n
seq . n in rng seq by VALUED_0:28;
then A8: seq . n in dom (h1 (#) h2) by A5;
thus ((h1 (#) h2) /* seq) . n = (h1 (#) h2) /. (seq . n) by A5, FUNCT_2:186
.= (h1 /. (seq . n)) * (h2 /. (seq . n)) by A8, CFUNCT_1:5
.= ((h1 /* seq) . n) * (h2 /. (seq . n)) by A1, A2, FUNCT_2:186, XBOOLE_1:1
.= ((h1 /* seq) . n) * ((h2 /* seq) . n) by A1, A2, FUNCT_2:186, XBOOLE_1:1
.= ((h1 /* seq) (#) (h2 /* seq)) . n by VALUED_1:5 ; :: thesis: verum

end;

hence (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) by FUNCT_2:113; :: thesis: verum