let X, Y be set ; :: thesis: for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,the carrier of V
for f1 being PartFunc of C,REAL st f1 | X is V8() & f2 | Y is V8() holds
(f1 (#) f2) | (X /\ Y) is V8()
let C be non empty set ; :: thesis: for V being RealNormSpace
for f2 being PartFunc of C,the carrier of V
for f1 being PartFunc of C,REAL st f1 | X is V8() & f2 | Y is V8() holds
(f1 (#) f2) | (X /\ Y) is V8()
let V be RealNormSpace; :: thesis: for f2 being PartFunc of C,the carrier of V
for f1 being PartFunc of C,REAL st f1 | X is V8() & f2 | Y is V8() holds
(f1 (#) f2) | (X /\ Y) is V8()
let f2 be PartFunc of C,the carrier of V; :: thesis: for f1 being PartFunc of C,REAL st f1 | X is V8() & f2 | Y is V8() holds
(f1 (#) f2) | (X /\ Y) is V8()
let f1 be PartFunc of C,REAL ; :: thesis: ( f1 | X is V8() & f2 | Y is V8() implies (f1 (#) f2) | (X /\ Y) is V8() )
assume A1: ( f1 | X is V8() & f2 | Y is V8() ) ; :: thesis: (f1 (#) f2) | (X /\ Y) is V8()
then consider r1 being Real such that
A2: for c being Element of C st c in X /\ (dom f1) holds
f1 . c = r1 by PARTFUN2:76;
consider r2 being VECTOR of V such that
A3: for c being Element of C st c in Y /\ (dom f2) holds
f2 /. c = r2 by A1, PARTFUN2:54;

now

let c be Element of C; :: thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies (f1 (#) f2) /. c = r1 * r2 )
assume c in (X /\ Y) /\ (dom (f1 (#) f2)) ; :: thesis: (f1 (#) f2) /. c = r1 * r2
then A4: ( c in X /\ Y & c in dom (f1 (#) f2) ) by XBOOLE_0:def 4;
then A5: ( c in X & c in Y & c in (dom f1) /\ (dom f2) ) by Def3, XBOOLE_0:def 4;
then ( c in dom f1 & c in dom f2 ) by XBOOLE_0:def 4;
then A6: ( c in X /\ (dom f1) & c in Y /\ (dom f2) ) by A5, XBOOLE_0:def 4;
thus (f1 (#) f2) /. c = (f1 . c) * (f2 /. c) by A4, Def3
.= r1 * (f2 /. c) by A2, A6
.= r1 * r2 by A3, A6 ; :: thesis: verum

end;

hence (f1 (#) f2) | (X /\ Y) is V8() by PARTFUN2:54; :: thesis: verum