let X, A be set ; :: thesis: for f being Function of X,REAL
for s being Real holds (s + f) .: A = s ++ (f .: A)
let f be Function of X,REAL; :: thesis: for s being Real holds (s + f) .: A = s ++ (f .: A)
let s be Real; :: thesis: (s + f) .: A = s ++ (f .: A)

now :: thesis: for x being object holds
( ( x in (s + f) .: A implies x in s ++ (f .: A) ) & ( x in s ++ (f .: A) implies x in (s + f) .: A ) )

let x be object ; :: thesis: ( ( x in (s + f) .: A implies x in s ++ (f .: A) ) & ( x in s ++ (f .: A) implies x in (s + f) .: A ) )

hereby :: thesis: ( x in s ++ (f .: A) implies x in (s + f) .: A )

assume x in (s + f) .: A ; :: thesis: x in s ++ (f .: A)
then consider x1 being object such that
A1: ( x1 in X & x1 in A & x = (s + f) . x1 ) by FUNCT_2:64;
( x = s + (f . x1) & f . x1 in f .: A ) by A1, FUNCT_2:35, VALUED_1:2;
then x in { (s + q3) where q3 is Real : q3 in f .: A } ;
hence x in s ++ (f .: A) by Lm5; :: thesis: verum

end;

assume x in s ++ (f .: A) ; :: thesis: x in (s + f) .: A
then x in { (s + q3) where q3 is Real : q3 in f .: A } by Lm5;
then consider r3 being Real such that
A2: x = s + r3 and
A3: r3 in f .: A ;
consider x1 being object such that
A4: x1 in X and
A5: x1 in A and
A6: r3 = f . x1 by A3, FUNCT_2:64;
x = (s + f) . x1 by A2, A4, A6, VALUED_1:2;
hence x in (s + f) .: A by A4, A5, FUNCT_2:35; :: thesis: verum

end;

hence (s + f) .: A = s ++ (f .: A) by TARSKI:2; :: thesis: verum