let R be Ring; for X being set
for f, g, h being Element of Funcs (X, the carrier of R) holds
( h = (ADD (X,R)) . (f,g) iff for x being object st x in X holds
h . x = the addF of R . ((f . x),(g . x)) )
let X be set ; for f, g, h being Element of Funcs (X, the carrier of R) holds
( h = (ADD (X,R)) . (f,g) iff for x being object st x in X holds
h . x = the addF of R . ((f . x),(g . x)) )
let f, g, h be Element of Funcs (X, the carrier of R); ( h = (ADD (X,R)) . (f,g) iff for x being object st x in X holds
h . x = the addF of R . ((f . x),(g . x)) )
thus
( h = (ADD (X,R)) . (f,g) implies for x being object st x in X holds
h . x = the addF of R . ((f . x),(g . x)) )
( ( for x being object st x in X holds
h . x = the addF of R . ((f . x),(g . x)) ) implies h = (ADD (X,R)) . (f,g) )proof
assume A1:
h = (ADD (X,R)) . (
f,
g)
;
for x being object st x in X holds
h . x = the addF of R . ((f . x),(g . x))
let x be
object ;
( x in X implies h . x = the addF of R . ((f . x),(g . x)) )
assume
x in X
;
h . x = the addF of R . ((f . x),(g . x))
then A2:
x in dom ( the addF of R .: (f,g))
by FUNCT_2:def 1;
thus h . x =
( the addF of R .: (f,g)) . x
by A1, Def6
.=
the
addF of
R . (
(f . x),
(g . x))
by A2, FUNCOP_1:22
;
verum
end;
assume A3:
for x being object st x in X holds
h . x = the addF of R . ((f . x),(g . x))
; h = (ADD (X,R)) . (f,g)
A5:
dom ((ADD (X,R)) . (f,g)) = X
by FUNCT_2:def 1;
for x being object st x in dom h holds
h . x = ((ADD (X,R)) . (f,g)) . x
proof
let x be
object ;
( x in dom h implies h . x = ((ADD (X,R)) . (f,g)) . x )
assume B5:
x in dom h
;
h . x = ((ADD (X,R)) . (f,g)) . x
then
x in X
;
then A7:
x in dom ( the addF of R .: (f,g))
by FUNCT_2:def 1;
thus h . x =
the
addF of
R . (
(f . x),
(g . x))
by A3, B5
.=
( the addF of R .: (f,g)) . x
by A7, FUNCOP_1:22
.=
((ADD (X,R)) . (f,g)) . x
by Def6
;
verum
end;
hence
h = (ADD (X,R)) . (f,g)
by FUNCT_2:def 1, A5; verum