:: The Modification of a Function by a Function
:: and the Iteration of the Composition of a Function
:: by Czes{\l}aw Byli\'nski
::
:: Received March 1, 1990
:: Copyright (c) 1990-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, FUNCT_1, TARSKI, ZFMISC_1, RELAT_1, FUNCOP_1, SUBSET_1,
PARTFUN1, FUNCT_2, ORDINAL1, FUNCT_4, REALSET1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, RELAT_1,
FUNCT_1, RELSET_1, REALSET1, FUNCT_2, BINOP_1, PARTFUN1, FUNCOP_1;
constructors PARTFUN1, BINOP_1, FUNCOP_1, RELSET_1, ORDINAL1, REALSET1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, RELSET_1, ZFMISC_1,
SUBSET_1, REALSET1;
requirements BOOLE, SUBSET;
begin :: Auxiliary theorems
reserve a,b,p,x,x9,x1,x19,x2,y,y9,y1,y19,y2,z,z9,z1,z2 for object,
X,X9,Y,Y9,Z,Z9 for set;
reserve A,D,D9 for non empty set;
reserve f,g,h for Function;
theorem :: FUNCT_4:1
(for z being object st z in Z holds ex x,y being object st z = [x,y])
implies ex X,Y st Z c= [:X,Y:];
theorem :: FUNCT_4:2
g*f = (g|rng f)*f;
theorem :: FUNCT_4:3
id X c= id Y iff X c= Y;
theorem :: FUNCT_4:4
X c= Y implies X --> a c= Y --> a;
theorem :: FUNCT_4:5
for a,b being object holds
X --> a c= Y --> b implies X c= Y;
theorem :: FUNCT_4:6
for a,b being object holds
X <> {} & X --> a c= Y --> b implies a = b;
theorem :: FUNCT_4:7
x in dom f implies x .--> f.x c= f;
:: Natural order on functions
theorem :: FUNCT_4:8
Y|`f|X c= f;
theorem :: FUNCT_4:9
f c= g implies Y|`f|X c= Y|`g|X;
definition
let f,g;
func f +* g -> Function means
:: FUNCT_4:def 1
dom it = dom f \/ dom g &
for x being object st x in dom f \/ dom g holds
(x in dom g implies it.x = g.x) &
(not x in dom g implies it.x = f.x);
idempotence;
end;
theorem :: FUNCT_4:10
dom f c= dom(f+*g) & dom g c= dom(f+*g);
theorem :: FUNCT_4:11
for x being object holds
not x in dom g implies (f +* g).x = f.x;
theorem :: FUNCT_4:12
for x being object holds
x in dom(f +* g) iff x in dom f or x in dom g;
theorem :: FUNCT_4:13
for x being object holds
x in dom g implies (f+*g).x = g.x;
theorem :: FUNCT_4:14
f +* g +* h = f +* (g +* h);
theorem :: FUNCT_4:15
f tolerates g & x in dom f implies (f+*g).x = f.x;
theorem :: FUNCT_4:16
dom f misses dom g & x in dom f implies (f +* g).x = f.x;
theorem :: FUNCT_4:17
rng(f +* g) c= rng f \/ rng g;
theorem :: FUNCT_4:18
rng g c= rng(f +* g);
theorem :: FUNCT_4:19
dom f c= dom g implies f +* g = g;
registration let f; let g be empty Function;
reduce g +* f to f;
reduce f +* g to f;
end;
theorem :: FUNCT_4:20
{} +* f = f;
theorem :: FUNCT_4:21
f +* {} = f;
theorem :: FUNCT_4:22
id(X) +* id(Y) = id(X \/ Y);
theorem :: FUNCT_4:23
(f +* g)|(dom g) = g;
theorem :: FUNCT_4:24
((f +* g)|(dom f \ dom g)) c= f;
theorem :: FUNCT_4:25
g c= f +* g;
theorem :: FUNCT_4:26
f tolerates g +* h implies f|(dom f \ dom h) tolerates g;
theorem :: FUNCT_4:27
f tolerates g +* h implies f tolerates h;
theorem :: FUNCT_4:28
f tolerates g iff f c= f +* g;
theorem :: FUNCT_4:29
f +* g c= f \/ g;
theorem :: FUNCT_4:30
f tolerates g iff f \/ g = f +* g;
theorem :: FUNCT_4:31
dom f misses dom g implies f \/ g = f +* g;
theorem :: FUNCT_4:32
dom f misses dom g implies f c= f +* g;
theorem :: FUNCT_4:33
dom f misses dom g implies (f +* g)|(dom f) = f;
theorem :: FUNCT_4:34
f tolerates g iff f +* g = g +* f;
theorem :: FUNCT_4:35
dom f misses dom g implies f +* g = g +* f;
theorem :: FUNCT_4:36
for f,g being PartFunc of X,Y st g is total holds f +* g = g;
theorem :: FUNCT_4:37
for f,g being Function of X,Y st Y = {} implies X = {} holds f +* g = g;
theorem :: FUNCT_4:38
for f,g being Function of X,X holds f +* g = g;
theorem :: FUNCT_4:39
for f,g being Function of X,D holds f +* g = g;
theorem :: FUNCT_4:40
for f,g being PartFunc of X,Y holds f +* g is PartFunc of X,Y;
:: The converse function whenever domain
definition
let f;
func ~f -> Function means
:: FUNCT_4:def 2
(for x being object holds x in dom it iff
ex y,z being object st x = [z,y] & [y,z] in dom f) &
for y,z being object st [y,z] in dom f holds it.(z,y) = f.(y,z);
end;
theorem :: FUNCT_4:41
rng ~f c= rng f;
theorem :: FUNCT_4:42
for x,y being object holds [x,y] in dom f iff [y,x] in dom ~f;
registration
let f be empty Function;
cluster ~f -> empty;
end;
theorem :: FUNCT_4:43
for x,y being object holds [y,x] in dom ~f implies (~f).(y,x) = f.(x,y);
theorem :: FUNCT_4:44
ex X,Y st dom ~f c= [:X,Y:];
theorem :: FUNCT_4:45
dom f c= [:X,Y:] implies dom ~f c= [:Y,X:];
theorem :: FUNCT_4:46
dom f = [:X,Y:] implies dom ~f = [:Y,X:];
theorem :: FUNCT_4:47
dom f c= [:X,Y:] implies rng ~f = rng f;
theorem :: FUNCT_4:48
for f being PartFunc of [:X,Y:],Z holds ~f is PartFunc of [:Y,X:],Z;
definition
let X,Y,Z;
let f be PartFunc of [:X,Y:],Z;
redefine func ~f -> PartFunc of [:Y,X:],Z;
end;
theorem :: FUNCT_4:49
for f being Function of [:X,Y:],Z holds ~f is Function of [:Y,X:],Z;
definition
let X,Y,Z;
let f be Function of [:X,Y:],Z;
redefine func ~f -> Function of [:Y,X:],Z;
end;
theorem :: FUNCT_4:50
for f being Function of [:X,Y:],Z holds ~f is Function of [:Y,X:],Z;
theorem :: FUNCT_4:51
~~f c= f;
theorem :: FUNCT_4:52
dom f c= [:X,Y:] implies ~~f = f;
theorem :: FUNCT_4:53
for f being PartFunc of [:X,Y:],Z holds ~~f = f;
:: Product of 2'ary functions
definition
let f,g;
func |:f,g:| -> Function means
:: FUNCT_4:def 3
(for z being object holds z in dom it
iff ex x,y,x9,y9 being object
st z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g) &
for x,y,x9,y9 being object
st [x,y] in dom f & [x9,y9] in dom g holds it.([x,x9],[y,y9]) = [f.(x,y),g.(x9,
y9)];
end;
theorem :: FUNCT_4:54
[[x,x9],[y,y9]] in dom |:f,g:| iff [x,y] in dom f & [x9,y9] in dom g;
theorem :: FUNCT_4:55
[[x,x9],[y,y9]] in dom |:f,g:| implies |:f,g:|.([x,x9],[y,y9]) = [f.(x
,y),g.(x9,y9)];
theorem :: FUNCT_4:56
rng |:f,g:| c= [:rng f,rng g:];
theorem :: FUNCT_4:57
dom f c= [:X,Y:] & dom g c= [:X9,Y9:] implies dom|:f,g:| c= [:[:
X,X9:],[:Y,Y9:]:];
theorem :: FUNCT_4:58
dom f = [:X,Y:] & dom g = [:X9,Y9:] implies
dom|:f,g:| = [:[:X,X9:],[:Y,Y9:]:];
theorem :: FUNCT_4:59
for f being PartFunc of [:X,Y:],Z for g being PartFunc of [:X9,Y9:],Z9
holds |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:];
theorem :: FUNCT_4:60
for f being Function of [:X,Y:],Z for g being Function of [:X9,
Y9:],Z9 st Z <> {} & Z9 <> {} holds |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]
:],[:Z,Z9:];
theorem :: FUNCT_4:61
for f being Function of [:X,Y:],D for g being Function of [:X9,Y9:],D9
holds |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:D,D9:];
definition
let x,y,a,b be object;
func (x,y) --> (a,b) -> set equals
:: FUNCT_4:def 4
(x .--> a) +* (y .--> b);
end;
registration
let x,y,a,b be object;
cluster (x,y) --> (a,b) -> Function-like Relation-like;
end;
theorem :: FUNCT_4:62
for x1,x2,y1,y2 being object holds
dom((x1,x2) --> (y1,y2)) = {x1,x2} & rng((x1,x2) --> (y1,y2)) c= {y1,y2};
theorem :: FUNCT_4:63
for x1,x2,y1,y2 being object holds
(x1 <> x2 implies ((x1,x2) --> (y1,y2)).x1 = y1) &
((x1,x2) --> (y1,y2)).x2 = y2;
theorem :: FUNCT_4:64
for x1,x2,y1,y2 being object holds
x1 <> x2 implies rng((x1,x2) --> (y1,y2)) = {y1,y2};
theorem :: FUNCT_4:65
for x1,x2,y being object holds
(x1,x2) --> (y,y) = {x1,x2} --> y;
definition
let A,x1,x2;
let y1,y2 be Element of A;
redefine func (x1,x2) --> (y1,y2) -> Function of {x1,x2},A;
end;
theorem :: FUNCT_4:66
for a,b,c,d being object, g being Function st dom g = {a,b} & g.a = c & g
.b = d holds g = (a,b) --> (c,d);
theorem :: FUNCT_4:67
for a,b,c,d being object st a <> c holds (a,c) --> (b,d) = { [a,b],
[c,d] };
theorem :: FUNCT_4:68
for a,b,x,y,x9,y9 being object st a <> b & (a,b) --> (x,y) = (a,b) --> (
x9,y9) holds x = x9 & y = y9;
begin :: Addenda
:: from CIRCCOMB
theorem :: FUNCT_4:69
for f1,f2, g1,g2 being Function st rng g1 c= dom f1 & rng g2 c= dom f2
& f1 tolerates f2 holds (f1+*f2)*(g1+*g2) = (f1*g1)+*(f2*g2);
:: from AMI_1
reserve A,B for set;
theorem :: FUNCT_4:70
dom f c= A \/ B implies f|A +* f|B = f;
:: from AMI_5
theorem :: FUNCT_4:71
for p,q being Function , A being set holds (p +* q)|A = p|A +* q|A;
theorem :: FUNCT_4:72
for f,g being Function, A being set st A misses dom g holds
(f +* g)|A = f|A;
theorem :: FUNCT_4:73
for f,g being Function , A being set holds dom f misses A implies
(f +* g)|A = g|A;
theorem :: FUNCT_4:74
for f,g,h being Function st dom g = dom h holds f +* g +* h = f +* h;
theorem :: FUNCT_4:75
for f being Function, A being set holds f +* f|A = f;
theorem :: FUNCT_4:76
for f,g being Function, B,C being set st dom f c= B & dom g c= C & B
misses C holds (f +* g)|B = f & (f +* g)|C = g;
theorem :: FUNCT_4:77
for p,q being Function, A being set holds dom p c= A & dom q misses A
implies (p +* q)|A = p;
theorem :: FUNCT_4:78
for f being Function, A,B being set holds f|(A \/ B) = f|A +* f|B;
:: from ALTCAT_1, CQC_LANG, 2007.03.13, A.T.
reserve x,y,i,j,k for object;
theorem :: FUNCT_4:79
(i,j):->k = [i,j].-->k;
theorem :: FUNCT_4:80
((i,j):->k).(i,j) = k;
:: from AMI_1, 2006.03.14, A.T.
theorem :: FUNCT_4:81
for a,b,c being object holds (a,a) --> (b,c) = a .--> c;
theorem :: FUNCT_4:82
for x,y holds x .--> y = {[x,y]};
:: from SCMPDS_9, 2006.03.26, A.T.
theorem :: FUNCT_4:83
for f being Function, a,b,c being object st a <> c holds (f +* (a .-->b))
.c = f.c;
theorem :: FUNCT_4:84
for f being Function, a,b,c,d being object st a <> b holds
(f +* ((a,b)-->(c,d))) .a = c & (f +* ((a,b)-->(c,d))) .b = d;
:: from AMI_3, 2007.06.14, A.T.
theorem :: FUNCT_4:85
for a,b being set, f being Function st a in dom f & f.a = b
holds a .--> b c= f;
theorem :: FUNCT_4:86
for a,b,c,d being set, f being Function st
a in dom f & c in dom f & f.a = b & f.c = d holds (a,c) --> (b,d) c= f;
:: from SCMFSA6A, 2007.07.23, A.T.
theorem :: FUNCT_4:87
for f,g,h being Function st f c= h & g c= h holds f +* g c= h;
:: from SCMFSA6B, 2007.07.25, A.T.
theorem :: FUNCT_4:88
for f, g being Function, A being set st A /\ dom f c= A /\ dom g holds
(f+*g|A)|A = g|A;
:: from SCMBSORT, 2007.07.26, A.T.
theorem :: FUNCT_4:89
for f be Function, a,b,n,m be object holds
(f +* (a .--> b) +* (m .--> n)).m = n;
theorem :: FUNCT_4:90
for f be Function, n,m be object holds (f +* (n .--> m) +* (m .--> n)).n=
m;
theorem :: FUNCT_4:91
for f be Function, a,b,n,m,x be object st x <> m & x <> a
holds (f +* (a.--> b) +* (m .--> n)).x=f.x;
:: from KNASTER, 2007.010.28, A.T.
theorem :: FUNCT_4:92
f is one-to-one & g is one-to-one & rng f misses rng g implies
f+*g is one-to-one;
registration let f,g be Function;
reduce f +* g +* g to f +* g;
end;
:: from SCMFSA_9, 2008.03.04, A.T.
theorem :: FUNCT_4:93
for f,g being Function holds f +* g +* g = f +* g;
theorem :: FUNCT_4:94
for f,g,h being Function, D being set holds (f +* g)|D =h | D implies
(h +* g) | D = (f +* g) | D;
theorem :: FUNCT_4:95
for f,g,h being Function, D being set holds f | D =h | D implies (h +*
g) | D = (f +* g) | D;
:: missing, 2008.03.20, A.T.
theorem :: FUNCT_4:96
x .--> x = id{x};
theorem :: FUNCT_4:97
f c= g implies f+*g = g;
theorem :: FUNCT_4:98
f c= g implies g+*f = g;
begin :: Changing a value in the range, 2008.03.20, A.T.
definition
let f,x,y;
func f+~(x,y) -> set equals
:: FUNCT_4:def 5
f+*((x .--> y)*f);
end;
registration
let f,x,y;
cluster f+~(x,y) -> Relation-like Function-like;
end;
theorem :: FUNCT_4:99
for x,y being object holds
dom(f+~(x,y)) = dom f;
theorem :: FUNCT_4:100
for x,y being object holds
x <> y implies not x in rng(f+~(x,y));
theorem :: FUNCT_4:101
for x,y being object holds
x in rng f implies y in rng(f+~(x,y));
theorem :: FUNCT_4:102
for x being object holds
f+~(x,x) = f;
theorem :: FUNCT_4:103
for x,y being object holds
not x in rng f implies f+~(x,y) = f;
theorem :: FUNCT_4:104
for x,y being object holds
rng(f+~(x,y)) c= rng f \ {x} \/ {y};
theorem :: FUNCT_4:105
for x,y,z being object holds
f.z <> x implies (f+~(x,y)).z = f.z;
theorem :: FUNCT_4:106
z in dom f & f.z = x implies (f+~(x,y)).z = y;
:: missing, 2008.04.06, A.T.
theorem :: FUNCT_4:107
not x in dom f implies f c= f +*(x .--> y);
theorem :: FUNCT_4:108
for f being PartFunc of X,Y, x,y st x in X & y in Y holds f+*(x .--> y
) is PartFunc of X,Y;
:: from FINSEQ_1, 2008.05.06, A.T.
registration
let f be Function, g be non empty Function;
cluster f +* g -> non empty;
cluster g +* f -> non empty;
end;
:: from CIRCCOMB, 2009.01.26, A.T.
registration
let f,g be non-empty Function;
cluster f+*g -> non-empty;
end;
definition let X,Y be set;
let f,g be PartFunc of X,Y;
redefine func f +* g -> PartFunc of X,Y;
end;
:: 2009.08.31, A.T.
reserve x for set;
theorem :: FUNCT_4:109
dom ((x --> y)+*(x .-->z)) = succ x;
theorem :: FUNCT_4:110
dom ((x --> y)+*(x .-->z)+*(succ x .-->z)) = succ succ x;
:: 2009.09.08, A.T.
reserve x for object;
registration let f,g be Function-yielding Function;
cluster f+*g -> Function-yielding;
end;
:: 2009.10.03, A.T.
registration
let I be set;
let f,g be I-defined Function;
cluster f+*g -> I-defined;
end;
registration
let I be set;
let f be total I-defined Function;
let g be I-defined Function;
cluster f+*g -> total for I-defined Function;
cluster g+*f -> total for I-defined Function;
end;
registration let I be set;
let g,h be I-valued Function;
cluster g+*h -> I-valued;
end;
registration let f be Function;
let g,h be f-compatible Function;
cluster g+*h -> f-compatible;
end;
:: missing, 2010.01.6, A.T
theorem :: FUNCT_4:111
f|A +* f = f;
:: from AMISTD_3, 2010.01.10, A.T
theorem :: FUNCT_4:112
for R being Relation st dom R = {x} & rng R = {y}
holds R = x .--> y;
theorem :: FUNCT_4:113
(f +* (x .-->y)).x = y;
theorem :: FUNCT_4:114
f +* (x .--> z1) +* (x .--> z2) = f +* (x .--> z2);
registration let A be non empty set, a,b be Element of A, x,y be set;
cluster (a,b) --> (x,y) -> A-defined;
end;
theorem :: FUNCT_4:115
dom g misses dom h implies f +* g +* h +* g = f +* g +* h;
theorem :: FUNCT_4:116
dom f misses dom h & f c= g +* h implies f c= g;
theorem :: FUNCT_4:117
dom f misses dom h & f c= g implies f c= g +* h;
theorem :: FUNCT_4:118
dom g misses dom h implies f +* g +* h = f +* h +* g;
theorem :: FUNCT_4:119
dom f misses dom g implies (f +* g) \ g = f;
theorem :: FUNCT_4:120
dom f misses dom g implies f \ g = f;
theorem :: FUNCT_4:121
dom g misses dom h implies (f \ g) +* h = (f +* h) \ g;
theorem :: FUNCT_4:122
for f1,f2,g1,g2 being Function
st f1 c= g1 & f2 c= g2 & dom f1 misses dom g2
holds f1 +* f2 c= g1 +* g2;
theorem :: FUNCT_4:123
for f, g, h being Function st f c= g holds f +* h c= g +* h;
theorem :: FUNCT_4:124
for f, g, h being Function st f c= g & dom f misses dom h holds f c= g +* h;
registration
let x, y be set;
cluster x .--> y -> trivial;
end;
:: from CIRCCOMB, 2011.04.19, A.T
theorem :: FUNCT_4:125
for f,g,h being Function st f tolerates g & g tolerates h & h
tolerates f holds f+*g tolerates h;
reserve A1,A2,B1,B2 for non empty set,
f for Function of A1,B1,
g for Function of A2,B2,
Y1 for non empty Subset of A1,
Y2 for non empty Subset of A2;
definition
let A,B be non empty set;
let f be PartFunc of [:A,A:],A;
let g be PartFunc of [:B,B:],B;
redefine func |:f,g:| -> PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:];
end;
theorem :: FUNCT_4:126
for f being PartFunc of [:A1,A1:],A1, g being PartFunc of [:A2,A2
:],A2 for F being PartFunc of [:Y1,Y1:],Y1 st F = f||Y1 for G being PartFunc of
[:Y2,Y2:],Y2 st G = g||Y2 holds |:F,G:| = |:f,g:| ||[:Y1,Y2:];
theorem :: FUNCT_4:127
for f being Function, x,y being object st x <> y
holds f+~(x,y)+~(x,z) = f+~(x,y);
:: 28.12.2012, A.T.
:: from BORSUK_7
reserve a,b,c,x,y,z,w,d for object;
definition
let a,b,c,x,y,z be object;
func (a,b,c) --> (x,y,z) -> set equals
:: FUNCT_4:def 6
((a,b) --> (x,y)) +* (c .--> z);
end;
registration
let a,b,c,x,y,z be object;
cluster (a,b,c) --> (x,y,z) -> Function-like Relation-like;
end;
theorem :: FUNCT_4:128
dom((a,b,c) --> (x,y,z)) = {a,b,c};
theorem :: FUNCT_4:129
rng((a,b,c) --> (x,y,z)) c= {x,y,z};
theorem :: FUNCT_4:130
(a,a,a) --> (x,y,z) = a .--> z;
theorem :: FUNCT_4:131
(a,a,b) --> (x,y,z) = (a,b) --> (y,z);
theorem :: FUNCT_4:132
a <> b implies (a,b,a) --> (x,y,z) = (a,b) --> (z,y);
theorem :: FUNCT_4:133
(a,b,b) --> (x,y,z) = (a,b) --> (x,z);
theorem :: FUNCT_4:134
a <> b & a <> c implies ((a,b,c) --> (x,y,z)).a = x;
theorem :: FUNCT_4:135
(b <> c implies ((a,b,c) --> (x,y,z)).b = y) &
((a,b,c) --> (x,y,z)).c = z;
theorem :: FUNCT_4:136
for f being Function st dom f = {a,b,c} & f.a = x & f.b = y & f.c = z holds
f = (a,b,c) --> (x,y,z);
:: from QUATERNI
definition
let x,y,w,z,a,b,c,d be object;
func (x,y,w,z) --> (a,b,c,d) -> set equals
:: FUNCT_4:def 7
((x,y) --> (a,b)) +* ((w,z) --> (c,d));
end;
registration
let x,y,w,z,a,b,c,d be object;
cluster (x,y,w,z) --> (a,b,c,d) -> Function-like Relation-like;
end;
theorem :: FUNCT_4:137
dom (x,y,w,z) --> (a,b,c,d) = {x,y,w,z};
theorem :: FUNCT_4:138
rng ((x,y,w,z) --> (a,b,c,d)) c= {a,b,c,d};
theorem :: FUNCT_4:139
((x,y,w,z) --> (a,b,c,d)).z=d;
theorem :: FUNCT_4:140
w <> z implies ((x,y,w,z) --> (a,b,c,d)).w=c;
theorem :: FUNCT_4:141
y <> w & y <> z implies
((x,y,w,z) --> (a,b,c,d)).y=b;
theorem :: FUNCT_4:142
x <> y & x <> w & x <> z implies
((x,y,w,z) --> (a,b,c,d)).x=a;
theorem :: FUNCT_4:143
x,y,w,z are_mutually_distinct implies
rng ((x,y,w,z) --> (a,b,c,d)) = {a,b,c,d};
theorem :: FUNCT_4:144
for a,b,c,d,e,i,j,k being object, g being Function
st dom g = {a,b,c,d} & g.a = e & g.b = i & g.c = j & g.d=k
holds g = (a,b,c,d) --> (e,i,j,k);
theorem :: FUNCT_4:145
for a,c,b,d,x,y,z,w being object holds
a,c,x,w are_mutually_distinct
implies (a,c,x,w) --> (b,d,y,z) = { [a,b], [c,d],[x,y],[w,z] };
theorem :: FUNCT_4:146
for a,b,c,d,x,y,z,w,x9,y9,z9,w9 being object
st a,b,c,d are_mutually_distinct &
(a,b,c,d) --> (x,y,z,w) = (a,b,c,d) --> (x9,y9,z9,w9)
holds x = x9 & y = y9 & z=z9 & w=w9;
:: from AOFA_A00
theorem :: FUNCT_4:147
for a1,a2,a3,b1,b2,b3 being object
st a1,a2,a3 are_mutually_distinct
holds
rng ((a1,a2,a3)-->(b1,b2,b3)) = {b1,b2,b3};
definition
let C,D,E be non empty set;
let f be Function of [:C,D:],E;
redefine func ~f -> Function of [:D,C:],E means
:: FUNCT_4:def 8
for d being Element of D, c being Element of C holds it.(d,c) = f.(c,d);
end;