let r be Real; :: thesis: for C, U being Subset of REAL
for f, g being Function of REAL,REAL holds r (#) ((f | C) +* (g | U)) = (r (#) (f | C)) +* (r (#) (g | U))
let C, U be Subset of REAL; :: thesis: for f, g being Function of REAL,REAL holds r (#) ((f | C) +* (g | U)) = (r (#) (f | C)) +* (r (#) (g | U))
let f, g be Function of REAL,REAL; :: thesis: r (#) ((f | C) +* (g | U)) = (r (#) (f | C)) +* (r (#) (g | U))
set f1 = r (#) ((f | C) +* (g | U));
set f2 = (r (#) (f | C)) +* (r (#) (g | U));
A3: dom (r (#) ((f | C) +* (g | U))) = dom ((f | C) +* (g | U)) by VALUED_1:def 5
.= (dom (f | C)) \/ (dom (g | U)) by FUNCT_4:def 1
.= C \/ (dom (g | U)) by FUNCT_2:def 1
.= C \/ U by FUNCT_2:def 1 ;
A1s: dom ((r (#) (f | C)) +* (r (#) (g | U))) = (dom (r (#) (f | C))) \/ (dom (r (#) (g | U))) by FUNCT_4:def 1
.= (dom (f | C)) \/ (dom (r (#) (g | U))) by VALUED_1:def 5
.= (dom (f | C)) \/ (dom (g | U)) by VALUED_1:def 5
.= C \/ (dom (g | U)) by FUNCT_2:def 1
.= C \/ U by FUNCT_2:def 1 ;
for x being object st x in dom (r (#) ((f | C) +* (g | U))) holds
(r (#) ((f | C) +* (g | U))) . x = ((r (#) (f | C)) +* (r (#) (g | U))) . x

proof

let x be object ; :: thesis: ( x in dom (r (#) ((f | C) +* (g | U))) implies (r (#) ((f | C) +* (g | U))) . x = ((r (#) (f | C)) +* (r (#) (g | U))) . x )
assume x in dom (r (#) ((f | C) +* (g | U))) ; :: thesis: (r (#) ((f | C) +* (g | U))) . x = ((r (#) (f | C)) +* (r (#) (g | U))) . x
then reconsider x = x as Real by A3;

per cases ( x in U or not x in U ) ;

suppose B1: x in U ; :: thesis: (r (#) ((f | C) +* (g | U))) . x = ((r (#) (f | C)) +* (r (#) (g | U))) . x

then B11: x in dom (g | U) by FUNCT_2:def 1;
B12: x in dom (r (#) (g | U)) by FUNCT_2:def 1, B1;
(r (#) ((f | C) +* (g | U))) . x = r * (((f | C) +* (g | U)) . x) by VALUED_1:6
.= r * ((g | U) . x) by B11, FUNCT_4:13
.= (r (#) (g | U)) . x by VALUED_1:6
.= ((r (#) (f | C)) +* (r (#) (g | U))) . x by FUNCT_4:13, B12 ;
hence (r (#) ((f | C) +* (g | U))) . x = ((r (#) (f | C)) +* (r (#) (g | U))) . x ; :: thesis: verum

end;

suppose B2: not x in U ; :: thesis: (r (#) ((f | C) +* (g | U))) . x = ((r (#) (f | C)) +* (r (#) (g | U))) . x

then B21: not x in dom (g | U) ;
B22: not x in dom (r (#) (g | U)) by B2;
(r (#) ((f | C) +* (g | U))) . x = r * (((f | C) +* (g | U)) . x) by VALUED_1:6
.= r * ((f | C) . x) by B21, FUNCT_4:11
.= (r (#) (f | C)) . x by VALUED_1:6
.= ((r (#) (f | C)) +* (r (#) (g | U))) . x by B22, FUNCT_4:11 ;
hence (r (#) ((f | C) +* (g | U))) . x = ((r (#) (f | C)) +* (r (#) (g | U))) . x ; :: thesis: verum

end;

end;

end;

hence r (#) ((f | C) +* (g | U)) = (r (#) (f | C)) +* (r (#) (g | U)) by FUNCT_1:2, A1s, A3; :: thesis: verum