let X, Y be non empty set ; for f1, f2 being V184() Function of [:X,Y:],ExtREAL holds ~ (f1 + f2) = (~ f1) + (~ f2)
let f1, f2 be V184() Function of [:X,Y:],ExtREAL; ~ (f1 + f2) = (~ f1) + (~ f2)
now for z being Element of [:Y,X:] holds (~ (f1 + f2)) . z = ((~ f1) + (~ f2)) . zlet z be
Element of
[:Y,X:];
(~ (f1 + f2)) . z = ((~ f1) + (~ f2)) . zconsider y,
x being
object such that A1:
(
y in Y &
x in X &
z = [y,x] )
by ZFMISC_1:def 2;
reconsider y =
y as
Element of
Y by A1;
reconsider x =
x as
Element of
X by A1;
reconsider z1 =
[x,y] as
Element of
[:X,Y:] by ZFMISC_1:87;
(~ (f1 + f2)) . z = (~ (f1 + f2)) . (
y,
x)
by A1;
then
(~ (f1 + f2)) . z = (f1 + f2) . (
x,
y)
by FUNCT_4:def 8;
then A2:
(~ (f1 + f2)) . z = (f1 . z1) + (f2 . z1)
by Th7;
(
f1 . z1 = f1 . (
x,
y) &
f2 . z1 = f2 . (
x,
y) )
;
then
(
f1 . z1 = (~ f1) . (
y,
x) &
f2 . z1 = (~ f2) . (
y,
x) )
by FUNCT_4:def 8;
hence
(~ (f1 + f2)) . z = ((~ f1) + (~ f2)) . z
by A1, A2, Th7;
verum end;
hence
~ (f1 + f2) = (~ f1) + (~ f2)
by FUNCT_2:def 8; verum