:: 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-2021 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; registration let f,g be Function; reduce (f +* g)|(dom g) to g; end; 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 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;