let X, Y be non empty set ; for f1 being V183() Function of [:X,Y:],ExtREAL
for f2 being V184() Function of [:X,Y:],ExtREAL holds
( ~ (f1 - f2) = (~ f1) - (~ f2) & ~ (f2 - f1) = (~ f2) - (~ f1) )
let f1 be V183() Function of [:X,Y:],ExtREAL; for f2 being V184() Function of [:X,Y:],ExtREAL holds
( ~ (f1 - f2) = (~ f1) - (~ f2) & ~ (f2 - f1) = (~ f2) - (~ f1) )
let f2 be V184() Function of [:X,Y:],ExtREAL; ( ~ (f1 - f2) = (~ f1) - (~ f2) & ~ (f2 - f1) = (~ f2) - (~ f1) )
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; ~ (f2 - f1) = (~ f2) - (~ f1)
now for z being Element of [:Y,X:] holds (~ (f2 - f1)) . z = ((~ f2) - (~ f1)) . zlet z be
Element of
[:Y,X:];
(~ (f2 - f1)) . z = ((~ f2) - (~ f1)) . 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;
(~ (f2 - f1)) . z = (~ (f2 - f1)) . (
y,
x)
by A1;
then
(~ (f2 - f1)) . z = (f2 - f1) . (
x,
y)
by FUNCT_4:def 8;
then A2:
(~ (f2 - f1)) . z = (f2 . z1) - (f1 . 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
(~ (f2 - f1)) . z = ((~ f2) - (~ f1)) . z
by A1, A2, Th7;
verum end;
hence
~ (f2 - f1) = (~ f2) - (~ f1)
by FUNCT_2:def 8; verum