let i, k be Element of NAT ; :: thesis: for f, g being PartFunc of (REAL i),REAL
for x being Element of REAL i holds (f * (reproj (k,x))) (#) (g * (reproj (k,x))) = (f (#) g) * (reproj (k,x))
let f1, f2 be PartFunc of (REAL i),REAL; :: thesis: for x being Element of REAL i holds (f1 * (reproj (k,x))) (#) (f2 * (reproj (k,x))) = (f1 (#) f2) * (reproj (k,x))
let x be Element of REAL i; :: thesis: (f1 * (reproj (k,x))) (#) (f2 * (reproj (k,x))) = (f1 (#) f2) * (reproj (k,x))
A1: dom (reproj (k,x)) = REAL by FUNCT_2:def 1;
A2: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def 4;
for s being Element of REAL holds
( s in dom ((f1 (#) f2) * (reproj (k,x))) iff s in dom ((f1 * (reproj (k,x))) (#) (f2 * (reproj (k,x)))) )

proof

let s be Element of REAL ; :: thesis: ( s in dom ((f1 (#) f2) * (reproj (k,x))) iff s in dom ((f1 * (reproj (k,x))) (#) (f2 * (reproj (k,x)))) )
( s in dom ((f1 (#) f2) * (reproj (k,x))) iff (reproj (k,x)) . s in (dom f1) /\ (dom f2) ) by A2, A1, FUNCT_1:11;
then ( s in dom ((f1 (#) f2) * (reproj (k,x))) iff ( (reproj (k,x)) . s in dom f1 & (reproj (k,x)) . s in dom f2 ) ) by XBOOLE_0:def 4;
then ( s in dom ((f1 (#) f2) * (reproj (k,x))) iff ( s in dom (f1 * (reproj (k,x))) & s in dom (f2 * (reproj (k,x))) ) ) by A1, FUNCT_1:11;
then ( s in dom ((f1 (#) f2) * (reproj (k,x))) iff s in (dom (f1 * (reproj (k,x)))) /\ (dom (f2 * (reproj (k,x)))) ) by XBOOLE_0:def 4;
hence ( s in dom ((f1 (#) f2) * (reproj (k,x))) iff s in dom ((f1 * (reproj (k,x))) (#) (f2 * (reproj (k,x)))) ) by VALUED_1:def 4; :: thesis: verum

end;

then for s being object holds
( s in dom ((f1 (#) f2) * (reproj (k,x))) iff s in dom ((f1 * (reproj (k,x))) (#) (f2 * (reproj (k,x)))) ) ;
then A3: dom ((f1 (#) f2) * (reproj (k,x))) = dom ((f1 * (reproj (k,x))) (#) (f2 * (reproj (k,x)))) by TARSKI:2;
for z being Element of REAL st z in dom ((f1 (#) f2) * (reproj (k,x))) holds
((f1 (#) f2) * (reproj (k,x))) . z = ((f1 * (reproj (k,x))) (#) (f2 * (reproj (k,x)))) . z

proof

let z be Element of REAL ; :: thesis: ( z in dom ((f1 (#) f2) * (reproj (k,x))) implies ((f1 (#) f2) * (reproj (k,x))) . z = ((f1 * (reproj (k,x))) (#) (f2 * (reproj (k,x)))) . z )
assume A4: z in dom ((f1 (#) f2) * (reproj (k,x))) ; :: thesis: ((f1 (#) f2) * (reproj (k,x))) . z = ((f1 * (reproj (k,x))) (#) (f2 * (reproj (k,x)))) . z
then (reproj (k,x)) . z in (dom f1) /\ (dom f2) by A2, FUNCT_1:11;
then ( (reproj (k,x)) . z in dom f1 & (reproj (k,x)) . z in dom f2 ) by XBOOLE_0:def 4;
then ( z in dom (f1 * (reproj (k,x))) & z in dom (f2 * (reproj (k,x))) ) by A1, FUNCT_1:11;
then A5: ( f1 . ((reproj (k,x)) . z) = (f1 * (reproj (k,x))) . z & f2 . ((reproj (k,x)) . z) = (f2 * (reproj (k,x))) . z ) by FUNCT_1:12;
thus ((f1 (#) f2) * (reproj (k,x))) . z = (f1 (#) f2) . ((reproj (k,x)) . z) by A4, FUNCT_1:12
.= (f1 . ((reproj (k,x)) . z)) * (f2 . ((reproj (k,x)) . z)) by VALUED_1:5
.= ((f1 * (reproj (k,x))) (#) (f2 * (reproj (k,x)))) . z by A3, A4, A5, VALUED_1:def 4 ; :: thesis: verum

end;

hence (f1 * (reproj (k,x))) (#) (f2 * (reproj (k,x))) = (f1 (#) f2) * (reproj (k,x)) by A3, PARTFUN1:5; :: thesis: verum