:: FUNCT_3 semantic presentation begin theorem Th1: :: FUNCT_3:1 for A, Y being set st A c= Y holds id A = (id Y) | A proof let A, Y be set ; ::_thesis: ( A c= Y implies id A = (id Y) | A ) assume A c= Y ; ::_thesis: id A = (id Y) | A hence id A = id (Y /\ A) by XBOOLE_1:28 .= (id Y) * (id A) by FUNCT_1:22 .= (id Y) | A by RELAT_1:65 ; ::_thesis: verum end; theorem Th2: :: FUNCT_3:2 for X being set for f, g being Function st X c= dom (g * f) holds f .: X c= dom g proof let X be set ; ::_thesis: for f, g being Function st X c= dom (g * f) holds f .: X c= dom g let f, g be Function; ::_thesis: ( X c= dom (g * f) implies f .: X c= dom g ) assume A1: X c= dom (g * f) ; ::_thesis: f .: X c= dom g let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: X or y in dom g ) assume y in f .: X ; ::_thesis: y in dom g then ex x being set st ( x in dom f & x in X & y = f . x ) by FUNCT_1:def_6; hence y in dom g by A1, FUNCT_1:11; ::_thesis: verum end; theorem Th3: :: FUNCT_3:3 for X being set for f, g being Function st X c= dom f & f .: X c= dom g holds X c= dom (g * f) proof let X be set ; ::_thesis: for f, g being Function st X c= dom f & f .: X c= dom g holds X c= dom (g * f) let f, g be Function; ::_thesis: ( X c= dom f & f .: X c= dom g implies X c= dom (g * f) ) assume that A1: X c= dom f and A2: f .: X c= dom g ; ::_thesis: X c= dom (g * f) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom (g * f) ) assume A3: x in X ; ::_thesis: x in dom (g * f) then f . x in f .: X by A1, FUNCT_1:def_6; hence x in dom (g * f) by A1, A2, A3, FUNCT_1:11; ::_thesis: verum end; theorem Th4: :: FUNCT_3:4 for Y being set for f, g being Function st Y c= rng (g * f) & g is one-to-one holds g " Y c= rng f proof let Y be set ; ::_thesis: for f, g being Function st Y c= rng (g * f) & g is one-to-one holds g " Y c= rng f let f, g be Function; ::_thesis: ( Y c= rng (g * f) & g is one-to-one implies g " Y c= rng f ) assume that A1: Y c= rng (g * f) and A2: g is one-to-one ; ::_thesis: g " Y c= rng f let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in g " Y or y in rng f ) assume A3: y in g " Y ; ::_thesis: y in rng f then A4: y in dom g by FUNCT_1:def_7; g . y in Y by A3, FUNCT_1:def_7; then consider x being set such that A5: x in dom (g * f) and A6: g . y = (g * f) . x by A1, FUNCT_1:def_3; A7: x in dom f by A5, FUNCT_1:11; ( g . y = g . (f . x) & f . x in dom g ) by A5, A6, FUNCT_1:11, FUNCT_1:12; then y = f . x by A2, A4, FUNCT_1:def_4; hence y in rng f by A7, FUNCT_1:def_3; ::_thesis: verum end; theorem Th5: :: FUNCT_3:5 for Y being set for f, g being Function st Y c= rng g & g " Y c= rng f holds Y c= rng (g * f) proof let Y be set ; ::_thesis: for f, g being Function st Y c= rng g & g " Y c= rng f holds Y c= rng (g * f) let f, g be Function; ::_thesis: ( Y c= rng g & g " Y c= rng f implies Y c= rng (g * f) ) assume that A1: Y c= rng g and A2: g " Y c= rng f ; ::_thesis: Y c= rng (g * f) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in rng (g * f) ) assume A3: y in Y ; ::_thesis: y in rng (g * f) then consider z being set such that A4: ( z in dom g & y = g . z ) by A1, FUNCT_1:def_3; z in g " Y by A3, A4, FUNCT_1:def_7; then consider x being set such that A5: ( x in dom f & z = f . x ) by A2, FUNCT_1:def_3; ( x in dom (g * f) & (g * f) . x = y ) by A4, A5, FUNCT_1:11, FUNCT_1:13; hence y in rng (g * f) by FUNCT_1:def_3; ::_thesis: verum end; scheme :: FUNCT_3:sch 1 FuncEx3{ F1() -> set , F2() -> set , P1[ set , set , set ] } : ex f being Function st ( dom f = [:F1(),F2():] & ( for x, y being set st x in F1() & y in F2() holds P1[x,y,f . (x,y)] ) ) provided A1: for x, y, z1, z2 being set st x in F1() & y in F2() & P1[x,y,z1] & P1[x,y,z2] holds z1 = z2 and A2: for x, y being set st x in F1() & y in F2() holds ex z being set st P1[x,y,z] proof defpred S1[ set , set ] means for x, y being set st \$1 = [x,y] holds P1[x,y,\$2]; set D = [:F1(),F2():]; A3: for p being set st p in [:F1(),F2():] holds ex z being set st S1[p,z] proof let p be set ; ::_thesis: ( p in [:F1(),F2():] implies ex z being set st S1[p,z] ) assume p in [:F1(),F2():] ; ::_thesis: ex z being set st S1[p,z] then consider x1, y1 being set such that A4: ( x1 in F1() & y1 in F2() ) and A5: p = [x1,y1] by ZFMISC_1:def_2; consider z being set such that A6: P1[x1,y1,z] by A2, A4; take z ; ::_thesis: S1[p,z] let x, y be set ; ::_thesis: ( p = [x,y] implies P1[x,y,z] ) assume A7: p = [x,y] ; ::_thesis: P1[x,y,z] then x = x1 by A5, XTUPLE_0:1; hence P1[x,y,z] by A5, A6, A7, XTUPLE_0:1; ::_thesis: verum end; A8: for p, y1, y2 being set st p in [:F1(),F2():] & S1[p,y1] & S1[p,y2] holds y1 = y2 proof let p, y1, y2 be set ; ::_thesis: ( p in [:F1(),F2():] & S1[p,y1] & S1[p,y2] implies y1 = y2 ) assume p in [:F1(),F2():] ; ::_thesis: ( not S1[p,y1] or not S1[p,y2] or y1 = y2 ) then consider x1, x2 being set such that A9: ( x1 in F1() & x2 in F2() ) and A10: p = [x1,x2] by ZFMISC_1:def_2; assume ( ( for x, y being set st p = [x,y] holds P1[x,y,y1] ) & ( for x, y being set st p = [x,y] holds P1[x,y,y2] ) ) ; ::_thesis: y1 = y2 then ( P1[x1,x2,y1] & P1[x1,x2,y2] ) by A10; hence y1 = y2 by A1, A9; ::_thesis: verum end; consider f being Function such that A11: dom f = [:F1(),F2():] and A12: for p being set st p in [:F1(),F2():] holds S1[p,f . p] from FUNCT_1:sch_2(A8, A3); take f ; ::_thesis: ( dom f = [:F1(),F2():] & ( for x, y being set st x in F1() & y in F2() holds P1[x,y,f . (x,y)] ) ) thus dom f = [:F1(),F2():] by A11; ::_thesis: for x, y being set st x in F1() & y in F2() holds P1[x,y,f . (x,y)] let x, y be set ; ::_thesis: ( x in F1() & y in F2() implies P1[x,y,f . (x,y)] ) assume ( x in F1() & y in F2() ) ; ::_thesis: P1[x,y,f . (x,y)] then [x,y] in [:F1(),F2():] by ZFMISC_1:def_2; hence P1[x,y,f . (x,y)] by A12; ::_thesis: verum end; scheme :: FUNCT_3:sch 2 Lambda3{ F1() -> set , F2() -> set , F3( set , set ) -> set } : ex f being Function st ( dom f = [:F1(),F2():] & ( for x, y being set st x in F1() & y in F2() holds f . (x,y) = F3(x,y) ) ) proof defpred S1[ set , set , set ] means \$3 = F3(\$1,\$2); A1: for x, y being set st x in F1() & y in F2() holds ex z being set st S1[x,y,z] ; A2: for x, y, z1, z2 being set st x in F1() & y in F2() & S1[x,y,z1] & S1[x,y,z2] holds z1 = z2 ; ex f being Function st ( dom f = [:F1(),F2():] & ( for x, y being set st x in F1() & y in F2() holds S1[x,y,f . (x,y)] ) ) from FUNCT_3:sch_1(A2, A1); hence ex f being Function st ( dom f = [:F1(),F2():] & ( for x, y being set st x in F1() & y in F2() holds f . (x,y) = F3(x,y) ) ) ; ::_thesis: verum end; theorem Th6: :: FUNCT_3:6 for X, Y being set for f, g being Function st dom f = [:X,Y:] & dom g = [:X,Y:] & ( for x, y being set st x in X & y in Y holds f . (x,y) = g . (x,y) ) holds f = g proof let X, Y be set ; ::_thesis: for f, g being Function st dom f = [:X,Y:] & dom g = [:X,Y:] & ( for x, y being set st x in X & y in Y holds f . (x,y) = g . (x,y) ) holds f = g let f, g be Function; ::_thesis: ( dom f = [:X,Y:] & dom g = [:X,Y:] & ( for x, y being set st x in X & y in Y holds f . (x,y) = g . (x,y) ) implies f = g ) assume that A1: ( dom f = [:X,Y:] & dom g = [:X,Y:] ) and A2: for x, y being set st x in X & y in Y holds f . (x,y) = g . (x,y) ; ::_thesis: f = g for p being set st p in [:X,Y:] holds f . p = g . p proof let p be set ; ::_thesis: ( p in [:X,Y:] implies f . p = g . p ) assume p in [:X,Y:] ; ::_thesis: f . p = g . p then consider x, y being set such that A3: ( x in X & y in Y ) and A4: p = [x,y] by ZFMISC_1:def_2; f . (x,y) = g . (x,y) by A2, A3; hence f . p = g . p by A4; ::_thesis: verum end; hence f = g by A1, FUNCT_1:2; ::_thesis: verum end; definition let f be Function; func .: f -> Function means :Def1: :: FUNCT_3:def 1 ( dom it = bool (dom f) & ( for X being set st X c= dom f holds it . X = f .: X ) ); existence ex b1 being Function st ( dom b1 = bool (dom f) & ( for X being set st X c= dom f holds b1 . X = f .: X ) ) proof defpred S1[ set , set ] means for X being set st \$1 = X holds \$2 = f .: X; A1: for x being set st x in bool (dom f) holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in bool (dom f) implies ex y being set st S1[x,y] ) assume x in bool (dom f) ; ::_thesis: ex y being set st S1[x,y] take f .: x ; ::_thesis: S1[x,f .: x] thus S1[x,f .: x] ; ::_thesis: verum end; A2: for x, y1, y2 being set st x in bool (dom f) & S1[x,y1] & S1[x,y2] holds y1 = y2 proof let x, y1, y2 be set ; ::_thesis: ( x in bool (dom f) & S1[x,y1] & S1[x,y2] implies y1 = y2 ) assume that x in bool (dom f) and A3: for X being set st x = X holds y1 = f .: X and A4: for X being set st x = X holds y2 = f .: X ; ::_thesis: y1 = y2 thus y1 = f .: x by A3 .= y2 by A4 ; ::_thesis: verum end; consider g being Function such that A5: ( dom g = bool (dom f) & ( for x being set st x in bool (dom f) holds S1[x,g . x] ) ) from FUNCT_1:sch_2(A2, A1); take g ; ::_thesis: ( dom g = bool (dom f) & ( for X being set st X c= dom f holds g . X = f .: X ) ) thus ( dom g = bool (dom f) & ( for X being set st X c= dom f holds g . X = f .: X ) ) by A5; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = bool (dom f) & ( for X being set st X c= dom f holds b1 . X = f .: X ) & dom b2 = bool (dom f) & ( for X being set st X c= dom f holds b2 . X = f .: X ) holds b1 = b2 proof let f1, f2 be Function; ::_thesis: ( dom f1 = bool (dom f) & ( for X being set st X c= dom f holds f1 . X = f .: X ) & dom f2 = bool (dom f) & ( for X being set st X c= dom f holds f2 . X = f .: X ) implies f1 = f2 ) assume that A6: dom f1 = bool (dom f) and A7: for X being set st X c= dom f holds f1 . X = f .: X and A8: dom f2 = bool (dom f) and A9: for X being set st X c= dom f holds f2 . X = f .: X ; ::_thesis: f1 = f2 for x being set st x in bool (dom f) holds f1 . x = f2 . x proof let x be set ; ::_thesis: ( x in bool (dom f) implies f1 . x = f2 . x ) assume A10: x in bool (dom f) ; ::_thesis: f1 . x = f2 . x then f1 . x = f .: x by A7; hence f1 . x = f2 . x by A9, A10; ::_thesis: verum end; hence f1 = f2 by A6, A8, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def1 defines .: FUNCT_3:def_1_:_ for f, b2 being Function holds ( b2 = .: f iff ( dom b2 = bool (dom f) & ( for X being set st X c= dom f holds b2 . X = f .: X ) ) ); theorem Th7: :: FUNCT_3:7 for X being set for f being Function st X in dom (.: f) holds (.: f) . X = f .: X proof let X be set ; ::_thesis: for f being Function st X in dom (.: f) holds (.: f) . X = f .: X let f be Function; ::_thesis: ( X in dom (.: f) implies (.: f) . X = f .: X ) assume X in dom (.: f) ; ::_thesis: (.: f) . X = f .: X then X in bool (dom f) by Def1; hence (.: f) . X = f .: X by Def1; ::_thesis: verum end; theorem :: FUNCT_3:8 for f being Function holds (.: f) . {} = {} proof let f be Function; ::_thesis: (.: f) . {} = {} {} c= dom f by XBOOLE_1:2; then (.: f) . {} = f .: {} by Def1; hence (.: f) . {} = {} ; ::_thesis: verum end; theorem Th9: :: FUNCT_3:9 for f being Function holds rng (.: f) c= bool (rng f) proof let f be Function; ::_thesis: rng (.: f) c= bool (rng f) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (.: f) or y in bool (rng f) ) assume y in rng (.: f) ; ::_thesis: y in bool (rng f) then consider x being set such that A1: ( x in dom (.: f) & y = (.: f) . x ) by FUNCT_1:def_3; y = f .: x by A1, Th7; then y c= rng f by RELAT_1:111; hence y in bool (rng f) ; ::_thesis: verum end; theorem :: FUNCT_3:10 for A being set for f being Function holds (.: f) .: A c= bool (rng f) proof let A be set ; ::_thesis: for f being Function holds (.: f) .: A c= bool (rng f) let f be Function; ::_thesis: (.: f) .: A c= bool (rng f) ( (.: f) .: A c= rng (.: f) & rng (.: f) c= bool (rng f) ) by Th9, RELAT_1:111; hence (.: f) .: A c= bool (rng f) by XBOOLE_1:1; ::_thesis: verum end; theorem Th11: :: FUNCT_3:11 for B being set for f being Function holds (.: f) " B c= bool (dom f) proof let B be set ; ::_thesis: for f being Function holds (.: f) " B c= bool (dom f) let f be Function; ::_thesis: (.: f) " B c= bool (dom f) dom (.: f) = bool (dom f) by Def1; hence (.: f) " B c= bool (dom f) by RELAT_1:132; ::_thesis: verum end; theorem :: FUNCT_3:12 for X, B being set for D being non empty set for f being Function of X,D holds (.: f) " B c= bool X proof let X, B be set ; ::_thesis: for D being non empty set for f being Function of X,D holds (.: f) " B c= bool X let D be non empty set ; ::_thesis: for f being Function of X,D holds (.: f) " B c= bool X let f be Function of X,D; ::_thesis: (.: f) " B c= bool X dom f = X by FUNCT_2:def_1; hence (.: f) " B c= bool X by Th11; ::_thesis: verum end; theorem Th13: :: FUNCT_3:13 for A being set for f being Function holds union ((.: f) .: A) c= f .: (union A) proof let A be set ; ::_thesis: for f being Function holds union ((.: f) .: A) c= f .: (union A) let f be Function; ::_thesis: union ((.: f) .: A) c= f .: (union A) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in union ((.: f) .: A) or y in f .: (union A) ) assume y in union ((.: f) .: A) ; ::_thesis: y in f .: (union A) then consider Z being set such that A1: y in Z and A2: Z in (.: f) .: A by TARSKI:def_4; consider X being set such that A3: X in dom (.: f) and A4: X in A and A5: Z = (.: f) . X by A2, FUNCT_1:def_6; y in f .: X by A1, A3, A5, Th7; then consider x being set such that A6: x in dom f and A7: x in X and A8: y = f . x by FUNCT_1:def_6; x in union A by A4, A7, TARSKI:def_4; hence y in f .: (union A) by A6, A8, FUNCT_1:def_6; ::_thesis: verum end; theorem Th14: :: FUNCT_3:14 for A being set for f being Function st A c= bool (dom f) holds f .: (union A) = union ((.: f) .: A) proof let A be set ; ::_thesis: for f being Function st A c= bool (dom f) holds f .: (union A) = union ((.: f) .: A) let f be Function; ::_thesis: ( A c= bool (dom f) implies f .: (union A) = union ((.: f) .: A) ) assume A1: A c= bool (dom f) ; ::_thesis: f .: (union A) = union ((.: f) .: A) A2: f .: (union A) c= union ((.: f) .: A) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: (union A) or y in union ((.: f) .: A) ) assume y in f .: (union A) ; ::_thesis: y in union ((.: f) .: A) then consider x being set such that x in dom f and A3: x in union A and A4: y = f . x by FUNCT_1:def_6; consider X being set such that A5: x in X and A6: X in A by A3, TARSKI:def_4; X in bool (dom f) by A1, A6; then X in dom (.: f) by Def1; then A7: (.: f) . X in (.: f) .: A by A6, FUNCT_1:def_6; y in f .: X by A1, A4, A5, A6, FUNCT_1:def_6; then y in (.: f) . X by A1, A6, Def1; hence y in union ((.: f) .: A) by A7, TARSKI:def_4; ::_thesis: verum end; union ((.: f) .: A) c= f .: (union A) by Th13; hence f .: (union A) = union ((.: f) .: A) by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: FUNCT_3:15 for X, A being set for D being non empty set for f being Function of X,D st A c= bool X holds f .: (union A) = union ((.: f) .: A) proof let X, A be set ; ::_thesis: for D being non empty set for f being Function of X,D st A c= bool X holds f .: (union A) = union ((.: f) .: A) let D be non empty set ; ::_thesis: for f being Function of X,D st A c= bool X holds f .: (union A) = union ((.: f) .: A) let f be Function of X,D; ::_thesis: ( A c= bool X implies f .: (union A) = union ((.: f) .: A) ) dom f = X by FUNCT_2:def_1; hence ( A c= bool X implies f .: (union A) = union ((.: f) .: A) ) by Th14; ::_thesis: verum end; theorem Th16: :: FUNCT_3:16 for B being set for f being Function holds union ((.: f) " B) c= f " (union B) proof let B be set ; ::_thesis: for f being Function holds union ((.: f) " B) c= f " (union B) let f be Function; ::_thesis: union ((.: f) " B) c= f " (union B) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union ((.: f) " B) or x in f " (union B) ) assume x in union ((.: f) " B) ; ::_thesis: x in f " (union B) then consider X being set such that A1: x in X and A2: X in (.: f) " B by TARSKI:def_4; dom (.: f) = bool (dom f) by Def1; then A3: X in bool (dom f) by A2, FUNCT_1:def_7; then A4: f . x in f .: X by A1, FUNCT_1:def_6; (.: f) . X in B by A2, FUNCT_1:def_7; then f .: X in B by A3, Def1; then f . x in union B by A4, TARSKI:def_4; hence x in f " (union B) by A1, A3, FUNCT_1:def_7; ::_thesis: verum end; theorem :: FUNCT_3:17 for B being set for f being Function st B c= bool (rng f) holds f " (union B) = union ((.: f) " B) proof let B be set ; ::_thesis: for f being Function st B c= bool (rng f) holds f " (union B) = union ((.: f) " B) let f be Function; ::_thesis: ( B c= bool (rng f) implies f " (union B) = union ((.: f) " B) ) assume A1: B c= bool (rng f) ; ::_thesis: f " (union B) = union ((.: f) " B) A2: f " (union B) c= union ((.: f) " B) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f " (union B) or x in union ((.: f) " B) ) assume A3: x in f " (union B) ; ::_thesis: x in union ((.: f) " B) then f . x in union B by FUNCT_1:def_7; then consider Y being set such that A4: f . x in Y and A5: Y in B by TARSKI:def_4; A6: f " Y c= dom f by RELAT_1:132; then f " Y in bool (dom f) ; then A7: f " Y in dom (.: f) by Def1; f .: (f " Y) = Y by A1, A5, FUNCT_1:77; then (.: f) . (f " Y) in B by A5, A6, Def1; then A8: f " Y in (.: f) " B by A7, FUNCT_1:def_7; x in dom f by A3, FUNCT_1:def_7; then x in f " Y by A4, FUNCT_1:def_7; hence x in union ((.: f) " B) by A8, TARSKI:def_4; ::_thesis: verum end; union ((.: f) " B) c= f " (union B) by Th16; hence f " (union B) = union ((.: f) " B) by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: FUNCT_3:18 for f, g being Function holds .: (g * f) = (.: g) * (.: f) proof let f, g be Function; ::_thesis: .: (g * f) = (.: g) * (.: f) for x being set holds ( x in dom (.: (g * f)) iff x in dom ((.: g) * (.: f)) ) proof let x be set ; ::_thesis: ( x in dom (.: (g * f)) iff x in dom ((.: g) * (.: f)) ) thus ( x in dom (.: (g * f)) implies x in dom ((.: g) * (.: f)) ) ::_thesis: ( x in dom ((.: g) * (.: f)) implies x in dom (.: (g * f)) ) proof assume x in dom (.: (g * f)) ; ::_thesis: x in dom ((.: g) * (.: f)) then A1: x in bool (dom (g * f)) by Def1; dom (g * f) c= dom f by RELAT_1:25; then A2: x c= dom f by A1, XBOOLE_1:1; then x in bool (dom f) ; then A3: x in dom (.: f) by Def1; f .: x c= dom g by A1, Th2; then f .: x in bool (dom g) ; then f .: x in dom (.: g) by Def1; then (.: f) . x in dom (.: g) by A2, Def1; hence x in dom ((.: g) * (.: f)) by A3, FUNCT_1:11; ::_thesis: verum end; assume A4: x in dom ((.: g) * (.: f)) ; ::_thesis: x in dom (.: (g * f)) then A5: x in dom (.: f) by FUNCT_1:11; (.: f) . x in dom (.: g) by A4, FUNCT_1:11; then f .: x in dom (.: g) by A5, Th7; then A6: f .: x in bool (dom g) by Def1; x in bool (dom f) by A5, Def1; then x c= dom (g * f) by A6, Th3; then x in bool (dom (g * f)) ; hence x in dom (.: (g * f)) by Def1; ::_thesis: verum end; then A7: dom (.: (g * f)) = dom ((.: g) * (.: f)) by TARSKI:1; for x being set st x in dom (.: (g * f)) holds (.: (g * f)) . x = ((.: g) * (.: f)) . x proof let x be set ; ::_thesis: ( x in dom (.: (g * f)) implies (.: (g * f)) . x = ((.: g) * (.: f)) . x ) assume A8: x in dom (.: (g * f)) ; ::_thesis: (.: (g * f)) . x = ((.: g) * (.: f)) . x then A9: x in bool (dom (g * f)) by Def1; then A10: f .: x c= dom g by Th2; dom (g * f) c= dom f by RELAT_1:25; then A11: x c= dom f by A9, XBOOLE_1:1; then x in bool (dom f) ; then A12: x in dom (.: f) by Def1; thus (.: (g * f)) . x = (g * f) .: x by A8, Th7 .= g .: (f .: x) by RELAT_1:126 .= (.: g) . (f .: x) by A10, Def1 .= (.: g) . ((.: f) . x) by A11, Def1 .= ((.: g) * (.: f)) . x by A12, FUNCT_1:13 ; ::_thesis: verum end; hence .: (g * f) = (.: g) * (.: f) by A7, FUNCT_1:2; ::_thesis: verum end; theorem Th19: :: FUNCT_3:19 for f being Function holds .: f is Function of (bool (dom f)),(bool (rng f)) proof let f be Function; ::_thesis: .: f is Function of (bool (dom f)),(bool (rng f)) ( dom (.: f) = bool (dom f) & rng (.: f) c= bool (rng f) ) by Def1, Th9; hence .: f is Function of (bool (dom f)),(bool (rng f)) by FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; theorem Th20: :: FUNCT_3:20 for X, Y being set for f being Function of X,Y st ( Y = {} implies X = {} ) holds .: f is Function of (bool X),(bool Y) proof let X, Y be set ; ::_thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) holds .: f is Function of (bool X),(bool Y) let f be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) implies .: f is Function of (bool X),(bool Y) ) assume ( Y = {} implies X = {} ) ; ::_thesis: .: f is Function of (bool X),(bool Y) then A1: dom f = X by FUNCT_2:def_1; rng f c= Y by RELAT_1:def_19; then A2: bool (rng f) c= bool Y by ZFMISC_1:67; A3: .: f is Function of (bool (dom f)),(bool (rng f)) by Th19; then rng (.: f) c= bool (rng f) by RELAT_1:def_19; then A4: rng (.: f) c= bool Y by A2, XBOOLE_1:1; dom (.: f) = bool (dom f) by A3, FUNCT_2:def_1; hence .: f is Function of (bool X),(bool Y) by A1, A4, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; definition let X be set ; let D be non empty set ; let f be Function of X,D; :: original: .: redefine func .: f -> Function of (bool X),(bool D); coherence .: f is Function of (bool X),(bool D) by Th20; end; definition let f be Function; func " f -> Function means :Def2: :: FUNCT_3:def 2 ( dom it = bool (rng f) & ( for Y being set st Y c= rng f holds it . Y = f " Y ) ); existence ex b1 being Function st ( dom b1 = bool (rng f) & ( for Y being set st Y c= rng f holds b1 . Y = f " Y ) ) proof defpred S1[ set , set ] means for Y being set st \$1 = Y holds \$2 = f " Y; A1: for y being set st y in bool (rng f) holds ex x being set st S1[y,x] proof let y be set ; ::_thesis: ( y in bool (rng f) implies ex x being set st S1[y,x] ) assume y in bool (rng f) ; ::_thesis: ex x being set st S1[y,x] take f " y ; ::_thesis: S1[y,f " y] thus S1[y,f " y] ; ::_thesis: verum end; A2: for y, x1, x2 being set st y in bool (rng f) & S1[y,x1] & S1[y,x2] holds x1 = x2 proof let y, x1, x2 be set ; ::_thesis: ( y in bool (rng f) & S1[y,x1] & S1[y,x2] implies x1 = x2 ) assume that y in bool (rng f) and A3: for Y being set st y = Y holds x1 = f " Y and A4: for Y being set st y = Y holds x2 = f " Y ; ::_thesis: x1 = x2 thus x1 = f " y by A3 .= x2 by A4 ; ::_thesis: verum end; consider g being Function such that A5: ( dom g = bool (rng f) & ( for y being set st y in bool (rng f) holds S1[y,g . y] ) ) from FUNCT_1:sch_2(A2, A1); take g ; ::_thesis: ( dom g = bool (rng f) & ( for Y being set st Y c= rng f holds g . Y = f " Y ) ) thus ( dom g = bool (rng f) & ( for Y being set st Y c= rng f holds g . Y = f " Y ) ) by A5; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = bool (rng f) & ( for Y being set st Y c= rng f holds b1 . Y = f " Y ) & dom b2 = bool (rng f) & ( for Y being set st Y c= rng f holds b2 . Y = f " Y ) holds b1 = b2 proof let f1, f2 be Function; ::_thesis: ( dom f1 = bool (rng f) & ( for Y being set st Y c= rng f holds f1 . Y = f " Y ) & dom f2 = bool (rng f) & ( for Y being set st Y c= rng f holds f2 . Y = f " Y ) implies f1 = f2 ) assume that A6: dom f1 = bool (rng f) and A7: for Y being set st Y c= rng f holds f1 . Y = f " Y and A8: dom f2 = bool (rng f) and A9: for Y being set st Y c= rng f holds f2 . Y = f " Y ; ::_thesis: f1 = f2 for y being set st y in bool (rng f) holds f1 . y = f2 . y proof let y be set ; ::_thesis: ( y in bool (rng f) implies f1 . y = f2 . y ) assume A10: y in bool (rng f) ; ::_thesis: f1 . y = f2 . y then f1 . y = f " y by A7; hence f1 . y = f2 . y by A9, A10; ::_thesis: verum end; hence f1 = f2 by A6, A8, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def2 defines " FUNCT_3:def_2_:_ for f, b2 being Function holds ( b2 = " f iff ( dom b2 = bool (rng f) & ( for Y being set st Y c= rng f holds b2 . Y = f " Y ) ) ); theorem Th21: :: FUNCT_3:21 for Y being set for f being Function st Y in dom (" f) holds (" f) . Y = f " Y proof let Y be set ; ::_thesis: for f being Function st Y in dom (" f) holds (" f) . Y = f " Y let f be Function; ::_thesis: ( Y in dom (" f) implies (" f) . Y = f " Y ) dom (" f) = bool (rng f) by Def2; hence ( Y in dom (" f) implies (" f) . Y = f " Y ) by Def2; ::_thesis: verum end; theorem Th22: :: FUNCT_3:22 for f being Function holds rng (" f) c= bool (dom f) proof let f be Function; ::_thesis: rng (" f) c= bool (dom f) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (" f) or x in bool (dom f) ) assume x in rng (" f) ; ::_thesis: x in bool (dom f) then consider y being set such that A1: ( y in dom (" f) & x = (" f) . y ) by FUNCT_1:def_3; x = f " y by A1, Th21; then x c= dom f by RELAT_1:132; hence x in bool (dom f) ; ::_thesis: verum end; theorem :: FUNCT_3:23 for B being set for f being Function holds (" f) .: B c= bool (dom f) proof let B be set ; ::_thesis: for f being Function holds (" f) .: B c= bool (dom f) let f be Function; ::_thesis: (" f) .: B c= bool (dom f) ( rng (" f) c= bool (dom f) & (" f) .: B c= rng (" f) ) by Th22, RELAT_1:111; hence (" f) .: B c= bool (dom f) by XBOOLE_1:1; ::_thesis: verum end; theorem :: FUNCT_3:24 for A being set for f being Function holds (" f) " A c= bool (rng f) proof let A be set ; ::_thesis: for f being Function holds (" f) " A c= bool (rng f) let f be Function; ::_thesis: (" f) " A c= bool (rng f) dom (" f) = bool (rng f) by Def2; hence (" f) " A c= bool (rng f) by RELAT_1:132; ::_thesis: verum end; theorem Th25: :: FUNCT_3:25 for B being set for f being Function holds union ((" f) .: B) c= f " (union B) proof let B be set ; ::_thesis: for f being Function holds union ((" f) .: B) c= f " (union B) let f be Function; ::_thesis: union ((" f) .: B) c= f " (union B) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union ((" f) .: B) or x in f " (union B) ) assume x in union ((" f) .: B) ; ::_thesis: x in f " (union B) then consider X being set such that A1: x in X and A2: X in (" f) .: B by TARSKI:def_4; consider Y being set such that A3: Y in dom (" f) and A4: Y in B and A5: X = (" f) . Y by A2, FUNCT_1:def_6; A6: (" f) . Y = f " Y by A3, Th21; Y in bool (rng f) by A3, Def2; then A7: f .: X in B by A4, A5, A6, FUNCT_1:77; A8: f " Y c= dom f by RELAT_1:132; then f . x in f .: X by A1, A5, A6, FUNCT_1:def_6; then f . x in union B by A7, TARSKI:def_4; hence x in f " (union B) by A1, A5, A6, A8, FUNCT_1:def_7; ::_thesis: verum end; theorem :: FUNCT_3:26 for B being set for f being Function st B c= bool (rng f) holds union ((" f) .: B) = f " (union B) proof let B be set ; ::_thesis: for f being Function st B c= bool (rng f) holds union ((" f) .: B) = f " (union B) let f be Function; ::_thesis: ( B c= bool (rng f) implies union ((" f) .: B) = f " (union B) ) assume A1: B c= bool (rng f) ; ::_thesis: union ((" f) .: B) = f " (union B) A2: f " (union B) c= union ((" f) .: B) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f " (union B) or x in union ((" f) .: B) ) assume A3: x in f " (union B) ; ::_thesis: x in union ((" f) .: B) then f . x in union B by FUNCT_1:def_7; then consider Y being set such that A4: f . x in Y and A5: Y in B by TARSKI:def_4; x in dom f by A3, FUNCT_1:def_7; then A6: x in f " Y by A4, FUNCT_1:def_7; Y in bool (rng f) by A1, A5; then A7: Y in dom (" f) by Def2; (" f) . Y = f " Y by A1, A5, Def2; then f " Y in (" f) .: B by A5, A7, FUNCT_1:def_6; hence x in union ((" f) .: B) by A6, TARSKI:def_4; ::_thesis: verum end; union ((" f) .: B) c= f " (union B) by Th25; hence union ((" f) .: B) = f " (union B) by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th27: :: FUNCT_3:27 for A being set for f being Function holds union ((" f) " A) c= f .: (union A) proof let A be set ; ::_thesis: for f being Function holds union ((" f) " A) c= f .: (union A) let f be Function; ::_thesis: union ((" f) " A) c= f .: (union A) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in union ((" f) " A) or y in f .: (union A) ) assume y in union ((" f) " A) ; ::_thesis: y in f .: (union A) then consider Y being set such that A1: y in Y and A2: Y in (" f) " A by TARSKI:def_4; dom (" f) = bool (rng f) by Def2; then A3: Y in bool (rng f) by A2, FUNCT_1:def_7; then consider x being set such that A4: ( x in dom f & y = f . x ) by A1, FUNCT_1:def_3; (" f) . Y in A by A2, FUNCT_1:def_7; then A5: f " Y in A by A3, Def2; x in f " Y by A1, A4, FUNCT_1:def_7; then x in union A by A5, TARSKI:def_4; hence y in f .: (union A) by A4, FUNCT_1:def_6; ::_thesis: verum end; theorem :: FUNCT_3:28 for A being set for f being Function st A c= bool (dom f) & f is one-to-one holds union ((" f) " A) = f .: (union A) proof let A be set ; ::_thesis: for f being Function st A c= bool (dom f) & f is one-to-one holds union ((" f) " A) = f .: (union A) let f be Function; ::_thesis: ( A c= bool (dom f) & f is one-to-one implies union ((" f) " A) = f .: (union A) ) assume that A1: A c= bool (dom f) and A2: f is one-to-one ; ::_thesis: union ((" f) " A) = f .: (union A) A3: f .: (union A) c= union ((" f) " A) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: (union A) or y in union ((" f) " A) ) assume y in f .: (union A) ; ::_thesis: y in union ((" f) " A) then consider x being set such that A4: x in dom f and A5: x in union A and A6: y = f . x by FUNCT_1:def_6; consider X being set such that A7: x in X and A8: X in A by A5, TARSKI:def_4; A9: f " (f .: X) c= X by A2, FUNCT_1:82; A10: f .: X c= rng f by RELAT_1:111; then f .: X in bool (rng f) ; then A11: f .: X in dom (" f) by Def2; X c= f " (f .: X) by A1, A8, FUNCT_1:76; then f " (f .: X) = X by A9, XBOOLE_0:def_10; then (" f) . (f .: X) in A by A8, A10, Def2; then A12: f .: X in (" f) " A by A11, FUNCT_1:def_7; y in f .: X by A4, A6, A7, FUNCT_1:def_6; hence y in union ((" f) " A) by A12, TARSKI:def_4; ::_thesis: verum end; union ((" f) " A) c= f .: (union A) by Th27; hence union ((" f) " A) = f .: (union A) by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th29: :: FUNCT_3:29 for B being set for f being Function holds (" f) .: B c= (.: f) " B proof let B be set ; ::_thesis: for f being Function holds (" f) .: B c= (.: f) " B let f be Function; ::_thesis: (" f) .: B c= (.: f) " B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (" f) .: B or x in (.: f) " B ) assume x in (" f) .: B ; ::_thesis: x in (.: f) " B then consider Y being set such that A1: Y in dom (" f) and A2: Y in B and A3: x = (" f) . Y by FUNCT_1:def_6; A4: (" f) . Y = f " Y by A1, Th21; then A5: x c= dom f by A3, RELAT_1:132; then x in bool (dom f) ; then A6: x in dom (.: f) by Def1; Y in bool (rng f) by A1, Def2; then f .: x in B by A2, A3, A4, FUNCT_1:77; then (.: f) . x in B by A5, Def1; hence x in (.: f) " B by A6, FUNCT_1:def_7; ::_thesis: verum end; theorem :: FUNCT_3:30 for B being set for f being Function st f is one-to-one holds (" f) .: B = (.: f) " B proof let B be set ; ::_thesis: for f being Function st f is one-to-one holds (" f) .: B = (.: f) " B let f be Function; ::_thesis: ( f is one-to-one implies (" f) .: B = (.: f) " B ) assume A1: f is one-to-one ; ::_thesis: (" f) .: B = (.: f) " B A2: (.: f) " B c= (" f) .: B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (.: f) " B or x in (" f) .: B ) A3: f .: x c= rng f by RELAT_1:111; then f .: x in bool (rng f) ; then A4: f .: x in dom (" f) by Def2; assume A5: x in (.: f) " B ; ::_thesis: x in (" f) .: B then A6: x in dom (.: f) by FUNCT_1:def_7; then x in bool (dom f) by Def1; then A7: x c= f " (f .: x) by FUNCT_1:76; f " (f .: x) c= x by A1, FUNCT_1:82; then x = f " (f .: x) by A7, XBOOLE_0:def_10; then A8: x = (" f) . (f .: x) by A3, Def2; (.: f) . x in B by A5, FUNCT_1:def_7; then f .: x in B by A6, Th7; hence x in (" f) .: B by A8, A4, FUNCT_1:def_6; ::_thesis: verum end; (" f) .: B c= (.: f) " B by Th29; hence (" f) .: B = (.: f) " B by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th31: :: FUNCT_3:31 for f being Function for A being set st A c= bool (dom f) holds (" f) " A c= (.: f) .: A proof let f be Function; ::_thesis: for A being set st A c= bool (dom f) holds (" f) " A c= (.: f) .: A let A be set ; ::_thesis: ( A c= bool (dom f) implies (" f) " A c= (.: f) .: A ) assume A1: A c= bool (dom f) ; ::_thesis: (" f) " A c= (.: f) .: A let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (" f) " A or y in (.: f) .: A ) assume A2: y in (" f) " A ; ::_thesis: y in (.: f) .: A then A3: (" f) . y in A by FUNCT_1:def_7; y in dom (" f) by A2, FUNCT_1:def_7; then A4: y in bool (rng f) by Def2; then A5: f " y in A by A3, Def2; then f " y in bool (dom f) by A1; then A6: f " y in dom (.: f) by Def1; f .: (f " y) = y by A4, FUNCT_1:77; then A7: (.: f) . (f " y) = y by A1, A5, Def1; f " y in A by A3, A4, Def2; hence y in (.: f) .: A by A7, A6, FUNCT_1:def_6; ::_thesis: verum end; theorem Th32: :: FUNCT_3:32 for f being Function for A being set st f is one-to-one holds (.: f) .: A c= (" f) " A proof let f be Function; ::_thesis: for A being set st f is one-to-one holds (.: f) .: A c= (" f) " A let A be set ; ::_thesis: ( f is one-to-one implies (.: f) .: A c= (" f) " A ) assume A1: f is one-to-one ; ::_thesis: (.: f) .: A c= (" f) " A let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (.: f) .: A or y in (" f) " A ) assume y in (.: f) .: A ; ::_thesis: y in (" f) " A then consider x being set such that A2: x in dom (.: f) and A3: x in A and A4: y = (.: f) . x by FUNCT_1:def_6; A5: x in bool (dom f) by A2, Def1; then A6: y = f .: x by A4, Def1; then A7: x c= f " y by A5, FUNCT_1:76; A8: y c= rng f by A6, RELAT_1:111; then y in bool (rng f) ; then A9: y in dom (" f) by Def2; f " y c= x by A1, A6, FUNCT_1:82; then f " y in A by A3, A7, XBOOLE_0:def_10; then (" f) . y in A by A8, Def2; hence y in (" f) " A by A9, FUNCT_1:def_7; ::_thesis: verum end; theorem :: FUNCT_3:33 for f being Function for A being set st f is one-to-one & A c= bool (dom f) holds (" f) " A = (.: f) .: A proof let f be Function; ::_thesis: for A being set st f is one-to-one & A c= bool (dom f) holds (" f) " A = (.: f) .: A let A be set ; ::_thesis: ( f is one-to-one & A c= bool (dom f) implies (" f) " A = (.: f) .: A ) assume ( f is one-to-one & A c= bool (dom f) ) ; ::_thesis: (" f) " A = (.: f) .: A then ( (" f) " A c= (.: f) .: A & (.: f) .: A c= (" f) " A ) by Th31, Th32; hence (" f) " A = (.: f) .: A by XBOOLE_0:def_10; ::_thesis: verum end; theorem :: FUNCT_3:34 for f, g being Function st g is one-to-one holds " (g * f) = (" f) * (" g) proof let f, g be Function; ::_thesis: ( g is one-to-one implies " (g * f) = (" f) * (" g) ) assume A1: g is one-to-one ; ::_thesis: " (g * f) = (" f) * (" g) for y being set holds ( y in dom (" (g * f)) iff y in dom ((" f) * (" g)) ) proof let y be set ; ::_thesis: ( y in dom (" (g * f)) iff y in dom ((" f) * (" g)) ) thus ( y in dom (" (g * f)) implies y in dom ((" f) * (" g)) ) ::_thesis: ( y in dom ((" f) * (" g)) implies y in dom (" (g * f)) ) proof assume y in dom (" (g * f)) ; ::_thesis: y in dom ((" f) * (" g)) then A2: y in bool (rng (g * f)) by Def2; rng (g * f) c= rng g by RELAT_1:26; then A3: y c= rng g by A2, XBOOLE_1:1; then y in bool (rng g) ; then A4: y in dom (" g) by Def2; g " y c= rng f by A1, A2, Th4; then g " y in bool (rng f) ; then g " y in dom (" f) by Def2; then (" g) . y in dom (" f) by A3, Def2; hence y in dom ((" f) * (" g)) by A4, FUNCT_1:11; ::_thesis: verum end; assume A5: y in dom ((" f) * (" g)) ; ::_thesis: y in dom (" (g * f)) then A6: y in dom (" g) by FUNCT_1:11; (" g) . y in dom (" f) by A5, FUNCT_1:11; then g " y in dom (" f) by A6, Th21; then A7: g " y in bool (rng f) by Def2; y in bool (rng g) by A6, Def2; then y c= rng (g * f) by A7, Th5; then y in bool (rng (g * f)) ; hence y in dom (" (g * f)) by Def2; ::_thesis: verum end; then A8: dom (" (g * f)) = dom ((" f) * (" g)) by TARSKI:1; for y being set st y in dom (" (g * f)) holds (" (g * f)) . y = ((" f) * (" g)) . y proof let y be set ; ::_thesis: ( y in dom (" (g * f)) implies (" (g * f)) . y = ((" f) * (" g)) . y ) assume A9: y in dom (" (g * f)) ; ::_thesis: (" (g * f)) . y = ((" f) * (" g)) . y then A10: y in bool (rng (g * f)) by Def2; then A11: g " y c= rng f by A1, Th4; rng (g * f) c= rng g by RELAT_1:26; then A12: y c= rng g by A10, XBOOLE_1:1; then y in bool (rng g) ; then A13: y in dom (" g) by Def2; thus (" (g * f)) . y = (g * f) " y by A9, Th21 .= f " (g " y) by RELAT_1:146 .= (" f) . (g " y) by A11, Def2 .= (" f) . ((" g) . y) by A12, Def2 .= ((" f) * (" g)) . y by A13, FUNCT_1:13 ; ::_thesis: verum end; hence " (g * f) = (" f) * (" g) by A8, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCT_3:35 for f being Function holds " f is Function of (bool (rng f)),(bool (dom f)) proof let f be Function; ::_thesis: " f is Function of (bool (rng f)),(bool (dom f)) ( dom (" f) = bool (rng f) & rng (" f) c= bool (dom f) ) by Def2, Th22; hence " f is Function of (bool (rng f)),(bool (dom f)) by FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; definition let A, X be set ; func chi (A,X) -> Function means :Def3: :: FUNCT_3:def 3 ( dom it = X & ( for x being set st x in X holds ( ( x in A implies it . x = 1 ) & ( not x in A implies it . x = {} ) ) ) ); existence ex b1 being Function st ( dom b1 = X & ( for x being set st x in X holds ( ( x in A implies b1 . x = 1 ) & ( not x in A implies b1 . x = {} ) ) ) ) proof defpred S1[ set , set ] means ( ( \$1 in A implies \$2 = 1 ) & ( not \$1 in A implies \$2 = {} ) ); A1: for x being set st x in X holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in X implies ex y being set st S1[x,y] ) assume x in X ; ::_thesis: ex y being set st S1[x,y] ( not x in A implies ex y being set st ( y = {} & ( x in A implies y = 1 ) & ( not x in A implies y = {} ) ) ) ; hence ex y being set st S1[x,y] ; ::_thesis: verum end; A2: for x, y1, y2 being set st x in X & S1[x,y1] & S1[x,y2] holds y1 = y2 ; ex f being Function st ( dom f = X & ( for x being set st x in X holds S1[x,f . x] ) ) from FUNCT_1:sch_2(A2, A1); hence ex b1 being Function st ( dom b1 = X & ( for x being set st x in X holds ( ( x in A implies b1 . x = 1 ) & ( not x in A implies b1 . x = {} ) ) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = X & ( for x being set st x in X holds ( ( x in A implies b1 . x = 1 ) & ( not x in A implies b1 . x = {} ) ) ) & dom b2 = X & ( for x being set st x in X holds ( ( x in A implies b2 . x = 1 ) & ( not x in A implies b2 . x = {} ) ) ) holds b1 = b2 proof let f1, f2 be Function; ::_thesis: ( dom f1 = X & ( for x being set st x in X holds ( ( x in A implies f1 . x = 1 ) & ( not x in A implies f1 . x = {} ) ) ) & dom f2 = X & ( for x being set st x in X holds ( ( x in A implies f2 . x = 1 ) & ( not x in A implies f2 . x = {} ) ) ) implies f1 = f2 ) assume that A3: dom f1 = X and A4: for x being set st x in X holds ( ( x in A implies f1 . x = 1 ) & ( not x in A implies f1 . x = {} ) ) and A5: dom f2 = X and A6: for x being set st x in X holds ( ( x in A implies f2 . x = 1 ) & ( not x in A implies f2 . x = {} ) ) ; ::_thesis: f1 = f2 for x being set st x in X holds f1 . x = f2 . x proof let x be set ; ::_thesis: ( x in X implies f1 . x = f2 . x ) assume A7: x in X ; ::_thesis: f1 . x = f2 . x then A8: ( not x in A implies ( f1 . x = {} & f2 . x = {} ) ) by A4, A6; ( x in A implies ( f1 . x = 1 & f2 . x = 1 ) ) by A4, A6, A7; hence f1 . x = f2 . x by A8; ::_thesis: verum end; hence f1 = f2 by A3, A5, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def3 defines chi FUNCT_3:def_3_:_ for A, X being set for b3 being Function holds ( b3 = chi (A,X) iff ( dom b3 = X & ( for x being set st x in X holds ( ( x in A implies b3 . x = 1 ) & ( not x in A implies b3 . x = {} ) ) ) ) ); theorem Th36: :: FUNCT_3:36 for x, A, X being set st (chi (A,X)) . x = 1 holds x in A proof let x, A, X be set ; ::_thesis: ( (chi (A,X)) . x = 1 implies x in A ) assume A1: (chi (A,X)) . x = 1 ; ::_thesis: x in A percases ( x in X or not x in X ) ; suppose x in X ; ::_thesis: x in A hence x in A by A1, Def3; ::_thesis: verum end; suppose not x in X ; ::_thesis: x in A then not x in dom (chi (A,X)) by Def3; hence x in A by A1, FUNCT_1:def_2; ::_thesis: verum end; end; end; theorem :: FUNCT_3:37 for x, X, A being set st x in X \ A holds (chi (A,X)) . x = {} proof let x, X, A be set ; ::_thesis: ( x in X \ A implies (chi (A,X)) . x = {} ) assume A1: x in X \ A ; ::_thesis: (chi (A,X)) . x = {} then not x in A by XBOOLE_0:def_5; hence (chi (A,X)) . x = {} by A1, Def3; ::_thesis: verum end; theorem :: FUNCT_3:38 for A, X, B being set st A c= X & B c= X & chi (A,X) = chi (B,X) holds A = B proof let A, X, B be set ; ::_thesis: ( A c= X & B c= X & chi (A,X) = chi (B,X) implies A = B ) assume that A1: A c= X and A2: B c= X and A3: chi (A,X) = chi (B,X) ; ::_thesis: A = B for x being set holds ( x in A iff x in B ) proof let x be set ; ::_thesis: ( x in A iff x in B ) thus ( x in A implies x in B ) ::_thesis: ( x in B implies x in A ) proof assume x in A ; ::_thesis: x in B then (chi (A,X)) . x = 1 by A1, Def3; hence x in B by A3, Th36; ::_thesis: verum end; assume x in B ; ::_thesis: x in A then (chi (B,X)) . x = 1 by A2, Def3; hence x in A by A3, Th36; ::_thesis: verum end; hence A = B by TARSKI:1; ::_thesis: verum end; theorem Th39: :: FUNCT_3:39 for A, X being set holds rng (chi (A,X)) c= {{},1} proof let A, X be set ; ::_thesis: rng (chi (A,X)) c= {{},1} let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (chi (A,X)) or y in {{},1} ) assume y in rng (chi (A,X)) ; ::_thesis: y in {{},1} then consider x being set such that A1: x in dom (chi (A,X)) and A2: y = (chi (A,X)) . x by FUNCT_1:def_3; A3: ( x in A or not x in A ) ; x in X by A1, Def3; then ( y = {} or y = 1 ) by A2, A3, Def3; hence y in {{},1} by TARSKI:def_2; ::_thesis: verum end; theorem :: FUNCT_3:40 for X being set for f being Function of X,{{},1} holds f = chi ((f " {1}),X) proof let X be set ; ::_thesis: for f being Function of X,{{},1} holds f = chi ((f " {1}),X) let f be Function of X,{{},1}; ::_thesis: f = chi ((f " {1}),X) now__::_thesis:_(_dom_f_=_X_&_(_for_x_being_set_st_x_in_X_holds_ (_(_x_in_f_"_{1}_implies_f_._x_=_1_)_&_(_not_x_in_f_"_{1}_implies_f_._x_=_{}_)_)_)_) thus A1: dom f = X by FUNCT_2:def_1; ::_thesis: for x being set st x in X holds ( ( x in f " {1} implies f . x = 1 ) & ( not x in f " {1} implies f . x = {} ) ) let x be set ; ::_thesis: ( x in X implies ( ( x in f " {1} implies f . x = 1 ) & ( not x in f " {1} implies f . x = {} ) ) ) assume A2: x in X ; ::_thesis: ( ( x in f " {1} implies f . x = 1 ) & ( not x in f " {1} implies f . x = {} ) ) thus ( x in f " {1} implies f . x = 1 ) ::_thesis: ( not x in f " {1} implies f . x = {} ) proof assume x in f " {1} ; ::_thesis: f . x = 1 then f . x in {1} by FUNCT_1:def_7; hence f . x = 1 by TARSKI:def_1; ::_thesis: verum end; assume not x in f " {1} ; ::_thesis: f . x = {} then not f . x in {1} by A1, A2, FUNCT_1:def_7; then A3: ( rng f c= {{},1} & f . x <> 1 ) by RELAT_1:def_19, TARSKI:def_1; f . x in rng f by A1, A2, FUNCT_1:def_3; hence f . x = {} by A3, TARSKI:def_2; ::_thesis: verum end; hence f = chi ((f " {1}),X) by Def3; ::_thesis: verum end; definition let A, X be set ; :: original: chi redefine func chi (A,X) -> Function of X,{{},1}; coherence chi (A,X) is Function of X,{{},1} proof ( dom (chi (A,X)) = X & rng (chi (A,X)) c= {{},1} ) by Def3, Th39; hence chi (A,X) is Function of X,{{},1} by FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; end; notation let Y be set ; let A be Subset of Y; synonym incl A for id Y; end; definition let Y be set ; let A be Subset of Y; :: original: incl redefine func incl A -> Function of A,Y; coherence incl is Function of A,Y proof A1: ( rng (id A) = A & dom (id A) = A ) ; thus incl is Function of A,Y by A1, FUNCT_2:2; ::_thesis: verum end; end; theorem :: FUNCT_3:41 for Y being set for A being Subset of Y holds incl A = (id Y) | A by Th1; theorem :: FUNCT_3:42 for x, Y being set for A being Subset of Y st x in A holds (incl A) . x in Y proof let x, Y be set ; ::_thesis: for A being Subset of Y st x in A holds (incl A) . x in Y let A be Subset of Y; ::_thesis: ( x in A implies (incl A) . x in Y ) assume A1: x in A ; ::_thesis: (incl A) . x in Y ( dom (incl A) = A & rng (incl A) = A ) ; then (incl A) . x in A by A1, FUNCT_1:def_3; hence (incl A) . x in Y ; ::_thesis: verum end; definition let X, Y be set ; func pr1 (X,Y) -> Function means :Def4: :: FUNCT_3:def 4 ( dom it = [:X,Y:] & ( for x, y being set st x in X & y in Y holds it . (x,y) = x ) ); existence ex b1 being Function st ( dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds b1 . (x,y) = x ) ) proof deffunc H1( set , set ) -> set = \$1; ex f being Function st ( dom f = [:X,Y:] & ( for x, y being set st x in X & y in Y holds f . (x,y) = H1(x,y) ) ) from FUNCT_3:sch_2(); hence ex b1 being Function st ( dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds b1 . (x,y) = x ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds b1 . (x,y) = x ) & dom b2 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds b2 . (x,y) = x ) holds b1 = b2 proof let f1, f2 be Function; ::_thesis: ( dom f1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds f1 . (x,y) = x ) & dom f2 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds f2 . (x,y) = x ) implies f1 = f2 ) assume that A1: dom f1 = [:X,Y:] and A2: for x, y being set st x in X & y in Y holds f1 . (x,y) = x and A3: dom f2 = [:X,Y:] and A4: for x, y being set st x in X & y in Y holds f2 . (x,y) = x ; ::_thesis: f1 = f2 for x, y being set st x in X & y in Y holds f1 . (x,y) = f2 . (x,y) proof let x, y be set ; ::_thesis: ( x in X & y in Y implies f1 . (x,y) = f2 . (x,y) ) assume A5: ( x in X & y in Y ) ; ::_thesis: f1 . (x,y) = f2 . (x,y) then f1 . (x,y) = x by A2; hence f1 . (x,y) = f2 . (x,y) by A4, A5; ::_thesis: verum end; hence f1 = f2 by A1, A3, Th6; ::_thesis: verum end; func pr2 (X,Y) -> Function means :Def5: :: FUNCT_3:def 5 ( dom it = [:X,Y:] & ( for x, y being set st x in X & y in Y holds it . (x,y) = y ) ); existence ex b1 being Function st ( dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds b1 . (x,y) = y ) ) proof deffunc H1( set , set ) -> set = \$2; ex f being Function st ( dom f = [:X,Y:] & ( for x, y being set st x in X & y in Y holds f . (x,y) = H1(x,y) ) ) from FUNCT_3:sch_2(); hence ex b1 being Function st ( dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds b1 . (x,y) = y ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds b1 . (x,y) = y ) & dom b2 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds b2 . (x,y) = y ) holds b1 = b2 proof let f1, f2 be Function; ::_thesis: ( dom f1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds f1 . (x,y) = y ) & dom f2 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds f2 . (x,y) = y ) implies f1 = f2 ) assume that A6: dom f1 = [:X,Y:] and A7: for x, y being set st x in X & y in Y holds f1 . (x,y) = y and A8: dom f2 = [:X,Y:] and A9: for x, y being set st x in X & y in Y holds f2 . (x,y) = y ; ::_thesis: f1 = f2 for x, y being set st x in X & y in Y holds f1 . (x,y) = f2 . (x,y) proof let x, y be set ; ::_thesis: ( x in X & y in Y implies f1 . (x,y) = f2 . (x,y) ) assume A10: ( x in X & y in Y ) ; ::_thesis: f1 . (x,y) = f2 . (x,y) then f1 . (x,y) = y by A7; hence f1 . (x,y) = f2 . (x,y) by A9, A10; ::_thesis: verum end; hence f1 = f2 by A6, A8, Th6; ::_thesis: verum end; end; :: deftheorem Def4 defines pr1 FUNCT_3:def_4_:_ for X, Y being set for b3 being Function holds ( b3 = pr1 (X,Y) iff ( dom b3 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds b3 . (x,y) = x ) ) ); :: deftheorem Def5 defines pr2 FUNCT_3:def_5_:_ for X, Y being set for b3 being Function holds ( b3 = pr2 (X,Y) iff ( dom b3 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds b3 . (x,y) = y ) ) ); theorem Th43: :: FUNCT_3:43 for X, Y being set holds rng (pr1 (X,Y)) c= X proof let X, Y be set ; ::_thesis: rng (pr1 (X,Y)) c= X let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (pr1 (X,Y)) or x in X ) assume x in rng (pr1 (X,Y)) ; ::_thesis: x in X then consider p being set such that A1: p in dom (pr1 (X,Y)) and A2: x = (pr1 (X,Y)) . p by FUNCT_1:def_3; p in [:X,Y:] by A1, Def4; then consider x1, y1 being set such that A3: ( x1 in X & y1 in Y ) and A4: p = [x1,y1] by ZFMISC_1:def_2; x = (pr1 (X,Y)) . (x1,y1) by A2, A4; hence x in X by A3, Def4; ::_thesis: verum end; theorem :: FUNCT_3:44 for Y, X being set st Y <> {} holds rng (pr1 (X,Y)) = X proof let Y, X be set ; ::_thesis: ( Y <> {} implies rng (pr1 (X,Y)) = X ) set y = the Element of Y; assume A1: Y <> {} ; ::_thesis: rng (pr1 (X,Y)) = X A2: X c= rng (pr1 (X,Y)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in rng (pr1 (X,Y)) ) assume A3: x in X ; ::_thesis: x in rng (pr1 (X,Y)) then [x, the Element of Y] in [:X,Y:] by A1, ZFMISC_1:87; then A4: [x, the Element of Y] in dom (pr1 (X,Y)) by Def4; (pr1 (X,Y)) . (x, the Element of Y) = x by A1, A3, Def4; hence x in rng (pr1 (X,Y)) by A4, FUNCT_1:def_3; ::_thesis: verum end; rng (pr1 (X,Y)) c= X by Th43; hence rng (pr1 (X,Y)) = X by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th45: :: FUNCT_3:45 for X, Y being set holds rng (pr2 (X,Y)) c= Y proof let X, Y be set ; ::_thesis: rng (pr2 (X,Y)) c= Y let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (pr2 (X,Y)) or y in Y ) assume y in rng (pr2 (X,Y)) ; ::_thesis: y in Y then consider p being set such that A1: p in dom (pr2 (X,Y)) and A2: y = (pr2 (X,Y)) . p by FUNCT_1:def_3; p in [:X,Y:] by A1, Def5; then consider x1, y1 being set such that A3: ( x1 in X & y1 in Y ) and A4: p = [x1,y1] by ZFMISC_1:def_2; y = (pr2 (X,Y)) . (x1,y1) by A2, A4; hence y in Y by A3, Def5; ::_thesis: verum end; theorem :: FUNCT_3:46 for X, Y being set st X <> {} holds rng (pr2 (X,Y)) = Y proof let X, Y be set ; ::_thesis: ( X <> {} implies rng (pr2 (X,Y)) = Y ) set x = the Element of X; assume A1: X <> {} ; ::_thesis: rng (pr2 (X,Y)) = Y A2: Y c= rng (pr2 (X,Y)) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in rng (pr2 (X,Y)) ) assume A3: y in Y ; ::_thesis: y in rng (pr2 (X,Y)) then [ the Element of X,y] in [:X,Y:] by A1, ZFMISC_1:87; then A4: [ the Element of X,y] in dom (pr2 (X,Y)) by Def5; (pr2 (X,Y)) . ( the Element of X,y) = y by A1, A3, Def5; hence y in rng (pr2 (X,Y)) by A4, FUNCT_1:def_3; ::_thesis: verum end; rng (pr2 (X,Y)) c= Y by Th45; hence rng (pr2 (X,Y)) = Y by A2, XBOOLE_0:def_10; ::_thesis: verum end; definition let X, Y be set ; :: original: pr1 redefine func pr1 (X,Y) -> Function of [:X,Y:],X; coherence pr1 (X,Y) is Function of [:X,Y:],X proof percases not ( X = {} & not [:X,Y:] = {} & not ( X = {} & [:X,Y:] <> {} ) ) ; suppose ( X = {} implies [:X,Y:] = {} ) ; ::_thesis: pr1 (X,Y) is Function of [:X,Y:],X ( dom (pr1 (X,Y)) = [:X,Y:] & rng (pr1 (X,Y)) c= X ) by Def4, Th43; hence pr1 (X,Y) is Function of [:X,Y:],X by FUNCT_2:2; ::_thesis: verum end; suppose ( X = {} & [:X,Y:] <> {} ) ; ::_thesis: pr1 (X,Y) is Function of [:X,Y:],X hence pr1 (X,Y) is Function of [:X,Y:],X by ZFMISC_1:90; ::_thesis: verum end; end; end; :: original: pr2 redefine func pr2 (X,Y) -> Function of [:X,Y:],Y; coherence pr2 (X,Y) is Function of [:X,Y:],Y proof percases not ( Y = {} & not [:X,Y:] = {} & not ( Y = {} & [:X,Y:] <> {} ) ) ; suppose ( Y = {} implies [:X,Y:] = {} ) ; ::_thesis: pr2 (X,Y) is Function of [:X,Y:],Y ( dom (pr2 (X,Y)) = [:X,Y:] & rng (pr2 (X,Y)) c= Y ) by Def5, Th45; hence pr2 (X,Y) is Function of [:X,Y:],Y by FUNCT_2:2; ::_thesis: verum end; suppose ( Y = {} & [:X,Y:] <> {} ) ; ::_thesis: pr2 (X,Y) is Function of [:X,Y:],Y hence pr2 (X,Y) is Function of [:X,Y:],Y by ZFMISC_1:90; ::_thesis: verum end; end; end; end; definition let X be set ; func delta X -> Function means :Def6: :: FUNCT_3:def 6 ( dom it = X & ( for x being set st x in X holds it . x = [x,x] ) ); existence ex b1 being Function st ( dom b1 = X & ( for x being set st x in X holds b1 . x = [x,x] ) ) proof deffunc H1( set ) -> set = [\$1,\$1]; ex f being Function st ( dom f = X & ( for x being set st x in X holds f . x = H1(x) ) ) from FUNCT_1:sch_3(); hence ex b1 being Function st ( dom b1 = X & ( for x being set st x in X holds b1 . x = [x,x] ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = X & ( for x being set st x in X holds b1 . x = [x,x] ) & dom b2 = X & ( for x being set st x in X holds b2 . x = [x,x] ) holds b1 = b2 proof let f1, f2 be Function; ::_thesis: ( dom f1 = X & ( for x being set st x in X holds f1 . x = [x,x] ) & dom f2 = X & ( for x being set st x in X holds f2 . x = [x,x] ) implies f1 = f2 ) assume that A1: dom f1 = X and A2: for x being set st x in X holds f1 . x = [x,x] and A3: dom f2 = X and A4: for x being set st x in X holds f2 . x = [x,x] ; ::_thesis: f1 = f2 for x being set st x in X holds f1 . x = f2 . x proof let x be set ; ::_thesis: ( x in X implies f1 . x = f2 . x ) assume A5: x in X ; ::_thesis: f1 . x = f2 . x then f1 . x = [x,x] by A2; hence f1 . x = f2 . x by A4, A5; ::_thesis: verum end; hence f1 = f2 by A1, A3, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def6 defines delta FUNCT_3:def_6_:_ for X being set for b2 being Function holds ( b2 = delta X iff ( dom b2 = X & ( for x being set st x in X holds b2 . x = [x,x] ) ) ); theorem Th47: :: FUNCT_3:47 for X being set holds rng (delta X) c= [:X,X:] proof let X be set ; ::_thesis: rng (delta X) c= [:X,X:] let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (delta X) or y in [:X,X:] ) assume y in rng (delta X) ; ::_thesis: y in [:X,X:] then consider x being set such that A1: x in dom (delta X) and A2: y = (delta X) . x by FUNCT_1:def_3; A3: x in X by A1, Def6; then y = [x,x] by A2, Def6; hence y in [:X,X:] by A3, ZFMISC_1:87; ::_thesis: verum end; definition let X be set ; :: original: delta redefine func delta X -> Function of X,[:X,X:]; coherence delta X is Function of X,[:X,X:] proof ( dom (delta X) = X & rng (delta X) c= [:X,X:] ) by Def6, Th47; hence delta X is Function of X,[:X,X:] by FUNCT_2:2; ::_thesis: verum end; end; definition let f, g be Function; func<:f,g:> -> Function means :Def7: :: FUNCT_3:def 7 ( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds it . x = [(f . x),(g . x)] ) ); existence ex b1 being Function st ( dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds b1 . x = [(f . x),(g . x)] ) ) proof deffunc H1( set ) -> set = [(f . \$1),(g . \$1)]; ex fg being Function st ( dom fg = (dom f) /\ (dom g) & ( for x being set st x in (dom f) /\ (dom g) holds fg . x = H1(x) ) ) from FUNCT_1:sch_3(); hence ex b1 being Function st ( dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds b1 . x = [(f . x),(g . x)] ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds b1 . x = [(f . x),(g . x)] ) & dom b2 = (dom f) /\ (dom g) & ( for x being set st x in dom b2 holds b2 . x = [(f . x),(g . x)] ) holds b1 = b2 proof let f1, f2 be Function; ::_thesis: ( dom f1 = (dom f) /\ (dom g) & ( for x being set st x in dom f1 holds f1 . x = [(f . x),(g . x)] ) & dom f2 = (dom f) /\ (dom g) & ( for x being set st x in dom f2 holds f2 . x = [(f . x),(g . x)] ) implies f1 = f2 ) assume that A1: dom f1 = (dom f) /\ (dom g) and A2: for x being set st x in dom f1 holds f1 . x = [(f . x),(g . x)] and A3: dom f2 = (dom f) /\ (dom g) and A4: for x being set st x in dom f2 holds f2 . x = [(f . x),(g . x)] ; ::_thesis: f1 = f2 for x being set st x in (dom f) /\ (dom g) holds f1 . x = f2 . x proof let x be set ; ::_thesis: ( x in (dom f) /\ (dom g) implies f1 . x = f2 . x ) assume A5: x in (dom f) /\ (dom g) ; ::_thesis: f1 . x = f2 . x then f1 . x = [(f . x),(g . x)] by A1, A2; hence f1 . x = f2 . x by A3, A4, A5; ::_thesis: verum end; hence f1 = f2 by A1, A3, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def7 defines <: FUNCT_3:def_7_:_ for f, g, b3 being Function holds ( b3 = <:f,g:> iff ( dom b3 = (dom f) /\ (dom g) & ( for x being set st x in dom b3 holds b3 . x = [(f . x),(g . x)] ) ) ); registration let f be empty Function; let g be Function; cluster<:f,g:> -> empty ; coherence <:f,g:> is empty proof dom f = {} ; then dom <:f,g:> = {} /\ (dom g) by Def7; hence <:f,g:> is empty ; ::_thesis: verum end; cluster<:g,f:> -> empty ; coherence <:g,f:> is empty proof dom f = {} ; then dom <:g,f:> = {} /\ (dom g) by Def7; hence <:g,f:> is empty ; ::_thesis: verum end; end; theorem Th48: :: FUNCT_3:48 for x being set for f, g being Function st x in (dom f) /\ (dom g) holds <:f,g:> . x = [(f . x),(g . x)] proof let x be set ; ::_thesis: for f, g being Function st x in (dom f) /\ (dom g) holds <:f,g:> . x = [(f . x),(g . x)] let f, g be Function; ::_thesis: ( x in (dom f) /\ (dom g) implies <:f,g:> . x = [(f . x),(g . x)] ) assume x in (dom f) /\ (dom g) ; ::_thesis: <:f,g:> . x = [(f . x),(g . x)] then x in dom <:f,g:> by Def7; hence <:f,g:> . x = [(f . x),(g . x)] by Def7; ::_thesis: verum end; theorem Th49: :: FUNCT_3:49 for x, X being set for f, g being Function st dom f = X & dom g = X & x in X holds <:f,g:> . x = [(f . x),(g . x)] proof let x, X be set ; ::_thesis: for f, g being Function st dom f = X & dom g = X & x in X holds <:f,g:> . x = [(f . x),(g . x)] let f, g be Function; ::_thesis: ( dom f = X & dom g = X & x in X implies <:f,g:> . x = [(f . x),(g . x)] ) assume ( dom f = X & dom g = X & x in X ) ; ::_thesis: <:f,g:> . x = [(f . x),(g . x)] then x in (dom f) /\ (dom g) ; then x in dom <:f,g:> by Def7; hence <:f,g:> . x = [(f . x),(g . x)] by Def7; ::_thesis: verum end; theorem Th50: :: FUNCT_3:50 for X being set for f, g being Function st dom f = X & dom g = X holds dom <:f,g:> = X proof let X be set ; ::_thesis: for f, g being Function st dom f = X & dom g = X holds dom <:f,g:> = X let f, g be Function; ::_thesis: ( dom f = X & dom g = X implies dom <:f,g:> = X ) dom <:f,g:> = (dom f) /\ (dom g) by Def7; hence ( dom f = X & dom g = X implies dom <:f,g:> = X ) ; ::_thesis: verum end; theorem Th51: :: FUNCT_3:51 for f, g being Function holds rng <:f,g:> c= [:(rng f),(rng g):] proof let f, g be Function; ::_thesis: rng <:f,g:> c= [:(rng f),(rng g):] let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng <:f,g:> or q in [:(rng f),(rng g):] ) assume q in rng <:f,g:> ; ::_thesis: q in [:(rng f),(rng g):] then consider x being set such that A1: x in dom <:f,g:> and A2: q = <:f,g:> . x by FUNCT_1:def_3; A3: x in (dom f) /\ (dom g) by A1, Def7; then x in dom f by XBOOLE_0:def_4; then A4: f . x in rng f by FUNCT_1:def_3; x in dom g by A3, XBOOLE_0:def_4; then A5: g . x in rng g by FUNCT_1:def_3; q = [(f . x),(g . x)] by A1, A2, Def7; hence q in [:(rng f),(rng g):] by A4, A5, ZFMISC_1:87; ::_thesis: verum end; theorem Th52: :: FUNCT_3:52 for Y, Z being set for f, g being Function st dom f = dom g & rng f c= Y & rng g c= Z holds ( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g ) proof let Y, Z be set ; ::_thesis: for f, g being Function st dom f = dom g & rng f c= Y & rng g c= Z holds ( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g ) let f, g be Function; ::_thesis: ( dom f = dom g & rng f c= Y & rng g c= Z implies ( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g ) ) assume that A1: dom f = dom g and A2: ( rng f c= Y & rng g c= Z ) ; ::_thesis: ( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g ) A3: [:(rng f),(rng g):] c= [:Y,Z:] by A2, ZFMISC_1:96; A4: rng <:f,g:> c= [:(rng f),(rng g):] by Th51; dom (pr1 (Y,Z)) = [:Y,Z:] by Def4; then A5: dom ((pr1 (Y,Z)) * <:f,g:>) = dom <:f,g:> by A3, A4, RELAT_1:27, XBOOLE_1:1; then A6: dom ((pr1 (Y,Z)) * <:f,g:>) = dom f by A1, Th50; for x being set st x in dom f holds ((pr1 (Y,Z)) * <:f,g:>) . x = f . x proof let x be set ; ::_thesis: ( x in dom f implies ((pr1 (Y,Z)) * <:f,g:>) . x = f . x ) assume A7: x in dom f ; ::_thesis: ((pr1 (Y,Z)) * <:f,g:>) . x = f . x then A8: ( f . x in rng f & g . x in rng g ) by A1, FUNCT_1:def_3; thus ((pr1 (Y,Z)) * <:f,g:>) . x = (pr1 (Y,Z)) . (<:f,g:> . x) by A6, A7, FUNCT_1:12 .= (pr1 (Y,Z)) . ((f . x),(g . x)) by A5, A6, A7, Def7 .= f . x by A2, A8, Def4 ; ::_thesis: verum end; hence (pr1 (Y,Z)) * <:f,g:> = f by A6, FUNCT_1:2; ::_thesis: (pr2 (Y,Z)) * <:f,g:> = g dom (pr2 (Y,Z)) = [:Y,Z:] by Def5; then A9: dom ((pr2 (Y,Z)) * <:f,g:>) = dom <:f,g:> by A3, A4, RELAT_1:27, XBOOLE_1:1; then A10: dom ((pr2 (Y,Z)) * <:f,g:>) = dom g by A1, Th50; for x being set st x in dom g holds ((pr2 (Y,Z)) * <:f,g:>) . x = g . x proof let x be set ; ::_thesis: ( x in dom g implies ((pr2 (Y,Z)) * <:f,g:>) . x = g . x ) assume A11: x in dom g ; ::_thesis: ((pr2 (Y,Z)) * <:f,g:>) . x = g . x then A12: ( f . x in rng f & g . x in rng g ) by A1, FUNCT_1:def_3; thus ((pr2 (Y,Z)) * <:f,g:>) . x = (pr2 (Y,Z)) . (<:f,g:> . x) by A10, A11, FUNCT_1:12 .= (pr2 (Y,Z)) . ((f . x),(g . x)) by A9, A10, A11, Def7 .= g . x by A2, A12, Def5 ; ::_thesis: verum end; hence (pr2 (Y,Z)) * <:f,g:> = g by A10, FUNCT_1:2; ::_thesis: verum end; theorem Th53: :: FUNCT_3:53 for X, Y being set holds <:(pr1 (X,Y)),(pr2 (X,Y)):> = id [:X,Y:] proof let X, Y be set ; ::_thesis: <:(pr1 (X,Y)),(pr2 (X,Y)):> = id [:X,Y:] ( dom (pr1 (X,Y)) = [:X,Y:] & dom (pr2 (X,Y)) = [:X,Y:] ) by Def4, Def5; then A1: dom <:(pr1 (X,Y)),(pr2 (X,Y)):> = [:X,Y:] by Th50; A2: for x, y being set st x in X & y in Y holds <:(pr1 (X,Y)),(pr2 (X,Y)):> . (x,y) = (id [:X,Y:]) . (x,y) proof let x, y be set ; ::_thesis: ( x in X & y in Y implies <:(pr1 (X,Y)),(pr2 (X,Y)):> . (x,y) = (id [:X,Y:]) . (x,y) ) assume A3: ( x in X & y in Y ) ; ::_thesis: <:(pr1 (X,Y)),(pr2 (X,Y)):> . (x,y) = (id [:X,Y:]) . (x,y) then A4: [x,y] in [:X,Y:] by ZFMISC_1:87; hence <:(pr1 (X,Y)),(pr2 (X,Y)):> . (x,y) = [((pr1 (X,Y)) . (x,y)),((pr2 (X,Y)) . (x,y))] by A1, Def7 .= [x,((pr2 (X,Y)) . (x,y))] by A3, Def4 .= [x,y] by A3, Def5 .= (id [:X,Y:]) . (x,y) by A4, FUNCT_1:18 ; ::_thesis: verum end; dom (id [:X,Y:]) = [:X,Y:] ; hence <:(pr1 (X,Y)),(pr2 (X,Y)):> = id [:X,Y:] by A1, A2, Th6; ::_thesis: verum end; theorem Th54: :: FUNCT_3:54 for f, g, h, k being Function st dom f = dom g & dom k = dom h & <:f,g:> = <:k,h:> holds ( f = k & g = h ) proof let f, g, h, k be Function; ::_thesis: ( dom f = dom g & dom k = dom h & <:f,g:> = <:k,h:> implies ( f = k & g = h ) ) assume that A1: dom f = dom g and A2: dom k = dom h and A3: <:f,g:> = <:k,h:> ; ::_thesis: ( f = k & g = h ) A4: dom <:f,g:> = dom f by A1, Th50; for x being set st x in dom f holds f . x = k . x proof let x be set ; ::_thesis: ( x in dom f implies f . x = k . x ) assume x in dom f ; ::_thesis: f . x = k . x then ( <:f,g:> . x = [(f . x),(g . x)] & <:k,h:> . x = [(k . x),(h . x)] ) by A3, A4, Def7; hence f . x = k . x by A3, XTUPLE_0:1; ::_thesis: verum end; hence f = k by A2, A3, A4, Th50, FUNCT_1:2; ::_thesis: g = h A5: dom <:f,g:> = dom g by A1, Th50; for x being set st x in dom g holds g . x = h . x proof let x be set ; ::_thesis: ( x in dom g implies g . x = h . x ) assume x in dom g ; ::_thesis: g . x = h . x then ( <:f,g:> . x = [(f . x),(g . x)] & <:k,h:> . x = [(k . x),(h . x)] ) by A3, A5, Def7; hence g . x = h . x by A3, XTUPLE_0:1; ::_thesis: verum end; hence g = h by A2, A3, A5, Th50, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCT_3:55 for f, g, h being Function holds <:(f * h),(g * h):> = <:f,g:> * h proof let f, g, h be Function; ::_thesis: <:(f * h),(g * h):> = <:f,g:> * h for x being set holds ( x in dom <:(f * h),(g * h):> iff x in dom (<:f,g:> * h) ) proof let x be set ; ::_thesis: ( x in dom <:(f * h),(g * h):> iff x in dom (<:f,g:> * h) ) thus ( x in dom <:(f * h),(g * h):> implies x in dom (<:f,g:> * h) ) ::_thesis: ( x in dom (<:f,g:> * h) implies x in dom <:(f * h),(g * h):> ) proof assume x in dom <:(f * h),(g * h):> ; ::_thesis: x in dom (<:f,g:> * h) then A1: x in (dom (f * h)) /\ (dom (g * h)) by Def7; then A2: x in dom (f * h) by XBOOLE_0:def_4; x in dom (g * h) by A1, XBOOLE_0:def_4; then A3: h . x in dom g by FUNCT_1:11; h . x in dom f by A2, FUNCT_1:11; then h . x in (dom f) /\ (dom g) by A3, XBOOLE_0:def_4; then A4: h . x in dom <:f,g:> by Def7; x in dom h by A2, FUNCT_1:11; hence x in dom (<:f,g:> * h) by A4, FUNCT_1:11; ::_thesis: verum end; assume A5: x in dom (<:f,g:> * h) ; ::_thesis: x in dom <:(f * h),(g * h):> then A6: x in dom h by FUNCT_1:11; h . x in dom <:f,g:> by A5, FUNCT_1:11; then A7: h . x in (dom f) /\ (dom g) by Def7; then h . x in dom g by XBOOLE_0:def_4; then A8: x in dom (g * h) by A6, FUNCT_1:11; h . x in dom f by A7, XBOOLE_0:def_4; then x in dom (f * h) by A6, FUNCT_1:11; then x in (dom (f * h)) /\ (dom (g * h)) by A8, XBOOLE_0:def_4; hence x in dom <:(f * h),(g * h):> by Def7; ::_thesis: verum end; then A9: dom <:(f * h),(g * h):> = dom (<:f,g:> * h) by TARSKI:1; for x being set st x in dom <:(f * h),(g * h):> holds <:(f * h),(g * h):> . x = (<:f,g:> * h) . x proof let x be set ; ::_thesis: ( x in dom <:(f * h),(g * h):> implies <:(f * h),(g * h):> . x = (<:f,g:> * h) . x ) assume A10: x in dom <:(f * h),(g * h):> ; ::_thesis: <:(f * h),(g * h):> . x = (<:f,g:> * h) . x then A11: x in (dom (f * h)) /\ (dom (g * h)) by Def7; then A12: x in dom (f * h) by XBOOLE_0:def_4; then A13: x in dom h by FUNCT_1:11; A14: x in dom (g * h) by A11, XBOOLE_0:def_4; then A15: h . x in dom g by FUNCT_1:11; h . x in dom f by A12, FUNCT_1:11; then A16: h . x in (dom f) /\ (dom g) by A15, XBOOLE_0:def_4; thus <:(f * h),(g * h):> . x = [((f * h) . x),((g * h) . x)] by A10, Def7 .= [(f . (h . x)),((g * h) . x)] by A12, FUNCT_1:12 .= [(f . (h . x)),(g . (h . x))] by A14, FUNCT_1:12 .= <:f,g:> . (h . x) by A16, Th48 .= (<:f,g:> * h) . x by A13, FUNCT_1:13 ; ::_thesis: verum end; hence <:(f * h),(g * h):> = <:f,g:> * h by A9, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCT_3:56 for A being set for f, g being Function holds <:f,g:> .: A c= [:(f .: A),(g .: A):] proof let A be set ; ::_thesis: for f, g being Function holds <:f,g:> .: A c= [:(f .: A),(g .: A):] let f, g be Function; ::_thesis: <:f,g:> .: A c= [:(f .: A),(g .: A):] let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in <:f,g:> .: A or y in [:(f .: A),(g .: A):] ) assume y in <:f,g:> .: A ; ::_thesis: y in [:(f .: A),(g .: A):] then consider x being set such that A1: x in dom <:f,g:> and A2: x in A and A3: y = <:f,g:> . x by FUNCT_1:def_6; A4: x in (dom f) /\ (dom g) by A1, Def7; then x in dom f by XBOOLE_0:def_4; then A5: f . x in f .: A by A2, FUNCT_1:def_6; x in dom g by A4, XBOOLE_0:def_4; then A6: g . x in g .: A by A2, FUNCT_1:def_6; y = [(f . x),(g . x)] by A1, A3, Def7; hence y in [:(f .: A),(g .: A):] by A5, A6, ZFMISC_1:def_2; ::_thesis: verum end; theorem :: FUNCT_3:57 for B being set for C being non empty set for f, g being Function holds <:f,g:> " [:B,C:] = (f " B) /\ (g " C) proof let B be set ; ::_thesis: for C being non empty set for f, g being Function holds <:f,g:> " [:B,C:] = (f " B) /\ (g " C) let C be non empty set ; ::_thesis: for f, g being Function holds <:f,g:> " [:B,C:] = (f " B) /\ (g " C) let f, g be Function; ::_thesis: <:f,g:> " [:B,C:] = (f " B) /\ (g " C) for x being set holds ( x in <:f,g:> " [:B,C:] iff x in (f " B) /\ (g " C) ) proof let x be set ; ::_thesis: ( x in <:f,g:> " [:B,C:] iff x in (f " B) /\ (g " C) ) thus ( x in <:f,g:> " [:B,C:] implies x in (f " B) /\ (g " C) ) ::_thesis: ( x in (f " B) /\ (g " C) implies x in <:f,g:> " [:B,C:] ) proof assume A1: x in <:f,g:> " [:B,C:] ; ::_thesis: x in (f " B) /\ (g " C) then <:f,g:> . x in [:B,C:] by FUNCT_1:def_7; then consider y1, y2 being set such that A2: y1 in B and A3: y2 in C and A4: <:f,g:> . x = [y1,y2] by ZFMISC_1:def_2; A5: x in dom <:f,g:> by A1, FUNCT_1:def_7; then A6: x in (dom f) /\ (dom g) by Def7; then A7: x in dom g by XBOOLE_0:def_4; A8: [y1,y2] = [(f . x),(g . x)] by A4, A5, Def7; then y2 = g . x by XTUPLE_0:1; then A9: x in g " C by A3, A7, FUNCT_1:def_7; A10: x in dom f by A6, XBOOLE_0:def_4; y1 = f . x by A8, XTUPLE_0:1; then x in f " B by A2, A10, FUNCT_1:def_7; hence x in (f " B) /\ (g " C) by A9, XBOOLE_0:def_4; ::_thesis: verum end; assume A11: x in (f " B) /\ (g " C) ; ::_thesis: x in <:f,g:> " [:B,C:] then A12: x in g " C by XBOOLE_0:def_4; then A13: x in dom g by FUNCT_1:def_7; A14: x in f " B by A11, XBOOLE_0:def_4; then x in dom f by FUNCT_1:def_7; then A15: x in (dom f) /\ (dom g) by A13, XBOOLE_0:def_4; then A16: x in dom <:f,g:> by Def7; A17: g . x in C by A12, FUNCT_1:def_7; f . x in B by A14, FUNCT_1:def_7; then [(f . x),(g . x)] in [:B,C:] by A17, ZFMISC_1:def_2; then <:f,g:> . x in [:B,C:] by A15, Th48; hence x in <:f,g:> " [:B,C:] by A16, FUNCT_1:def_7; ::_thesis: verum end; hence <:f,g:> " [:B,C:] = (f " B) /\ (g " C) by TARSKI:1; ::_thesis: verum end; theorem Th58: :: FUNCT_3:58 for X, Y, Z being set for f being Function of X,Y for g being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) holds <:f,g:> is Function of X,[:Y,Z:] proof let X, Y, Z be set ; ::_thesis: for f being Function of X,Y for g being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) holds <:f,g:> is Function of X,[:Y,Z:] let f be Function of X,Y; ::_thesis: for g being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) holds <:f,g:> is Function of X,[:Y,Z:] let g be Function of X,Z; ::_thesis: ( ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) implies <:f,g:> is Function of X,[:Y,Z:] ) assume A1: ( ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) ) ; ::_thesis: <:f,g:> is Function of X,[:Y,Z:] percases not ( [:Y,Z:] = {} & not X = {} & not ( [:Y,Z:] = {} & X <> {} ) ) ; suppose ( [:Y,Z:] = {} implies X = {} ) ; ::_thesis: <:f,g:> is Function of X,[:Y,Z:] ( rng f c= Y & rng g c= Z ) by RELAT_1:def_19; then A2: [:(rng f),(rng g):] c= [:Y,Z:] by ZFMISC_1:96; ( dom f = X & dom g = X ) by A1, FUNCT_2:def_1; then A3: dom <:f,g:> = X by Th50; rng <:f,g:> c= [:(rng f),(rng g):] by Th51; then rng <:f,g:> c= [:Y,Z:] by A2, XBOOLE_1:1; hence <:f,g:> is Function of X,[:Y,Z:] by A3, FUNCT_2:2; ::_thesis: verum end; suppose ( [:Y,Z:] = {} & X <> {} ) ; ::_thesis: <:f,g:> is Function of X,[:Y,Z:] hence <:f,g:> is Function of X,[:Y,Z:] by A1; ::_thesis: verum end; end; end; definition let X be set ; let D1, D2 be non empty set ; let f1 be Function of X,D1; let f2 be Function of X,D2; :: original: <: redefine func<:f1,f2:> -> Function of X,[:D1,D2:]; coherence <:f1,f2:> is Function of X,[:D1,D2:] by Th58; end; theorem :: FUNCT_3:59 for C, D1, D2 being non empty set for f1 being Function of C,D1 for f2 being Function of C,D2 for c being Element of C holds <:f1,f2:> . c = [(f1 . c),(f2 . c)] proof let C, D1, D2 be non empty set ; ::_thesis: for f1 being Function of C,D1 for f2 being Function of C,D2 for c being Element of C holds <:f1,f2:> . c = [(f1 . c),(f2 . c)] let f1 be Function of C,D1; ::_thesis: for f2 being Function of C,D2 for c being Element of C holds <:f1,f2:> . c = [(f1 . c),(f2 . c)] let f2 be Function of C,D2; ::_thesis: for c being Element of C holds <:f1,f2:> . c = [(f1 . c),(f2 . c)] let c be Element of C; ::_thesis: <:f1,f2:> . c = [(f1 . c),(f2 . c)] ( dom f1 = C & dom f2 = C ) by FUNCT_2:def_1; hence <:f1,f2:> . c = [(f1 . c),(f2 . c)] by Th49; ::_thesis: verum end; theorem :: FUNCT_3:60 for X, Y, Z being set for f being Function of X,Y for g being Function of X,Z holds rng <:f,g:> c= [:Y,Z:] proof let X, Y, Z be set ; ::_thesis: for f being Function of X,Y for g being Function of X,Z holds rng <:f,g:> c= [:Y,Z:] let f be Function of X,Y; ::_thesis: for g being Function of X,Z holds rng <:f,g:> c= [:Y,Z:] let g be Function of X,Z; ::_thesis: rng <:f,g:> c= [:Y,Z:] ( rng f c= Y & rng g c= Z ) by RELAT_1:def_19; then A1: [:(rng f),(rng g):] c= [:Y,Z:] by ZFMISC_1:96; rng <:f,g:> c= [:(rng f),(rng g):] by Th51; hence rng <:f,g:> c= [:Y,Z:] by A1, XBOOLE_1:1; ::_thesis: verum end; theorem Th61: :: FUNCT_3:61 for X, Y, Z being set for f being Function of X,Y for g being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) holds ( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g ) proof let X, Y, Z be set ; ::_thesis: for f being Function of X,Y for g being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) holds ( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g ) let f be Function of X,Y; ::_thesis: for g being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) holds ( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g ) let g be Function of X,Z; ::_thesis: ( ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) implies ( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g ) ) assume ( ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) ) ; ::_thesis: ( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g ) then A1: ( dom f = X & dom g = X ) by FUNCT_2:def_1; ( rng f c= Y & rng g c= Z ) by RELAT_1:def_19; hence ( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g ) by A1, Th52; ::_thesis: verum end; theorem :: FUNCT_3:62 for X being set for D1, D2 being non empty set for f being Function of X,D1 for g being Function of X,D2 holds ( (pr1 (D1,D2)) * <:f,g:> = f & (pr2 (D1,D2)) * <:f,g:> = g ) by Th61; theorem :: FUNCT_3:63 for X, Y, Z being set for f1, f2 being Function of X,Y for g1, g2 being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) & <:f1,g1:> = <:f2,g2:> holds ( f1 = f2 & g1 = g2 ) proof let X, Y, Z be set ; ::_thesis: for f1, f2 being Function of X,Y for g1, g2 being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) & <:f1,g1:> = <:f2,g2:> holds ( f1 = f2 & g1 = g2 ) let f1, f2 be Function of X,Y; ::_thesis: for g1, g2 being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) & <:f1,g1:> = <:f2,g2:> holds ( f1 = f2 & g1 = g2 ) let g1, g2 be Function of X,Z; ::_thesis: ( ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) & <:f1,g1:> = <:f2,g2:> implies ( f1 = f2 & g1 = g2 ) ) assume that A1: ( Y = {} implies X = {} ) and A2: ( Z = {} implies X = {} ) ; ::_thesis: ( not <:f1,g1:> = <:f2,g2:> or ( f1 = f2 & g1 = g2 ) ) A3: ( dom g1 = X & dom g2 = X ) by A2, FUNCT_2:def_1; ( dom f1 = X & dom f2 = X ) by A1, FUNCT_2:def_1; hence ( not <:f1,g1:> = <:f2,g2:> or ( f1 = f2 & g1 = g2 ) ) by A3, Th54; ::_thesis: verum end; theorem :: FUNCT_3:64 for X being set for D1, D2 being non empty set for f1, f2 being Function of X,D1 for g1, g2 being Function of X,D2 st <:f1,g1:> = <:f2,g2:> holds ( f1 = f2 & g1 = g2 ) proof let X be set ; ::_thesis: for D1, D2 being non empty set for f1, f2 being Function of X,D1 for g1, g2 being Function of X,D2 st <:f1,g1:> = <:f2,g2:> holds ( f1 = f2 & g1 = g2 ) let D1, D2 be non empty set ; ::_thesis: for f1, f2 being Function of X,D1 for g1, g2 being Function of X,D2 st <:f1,g1:> = <:f2,g2:> holds ( f1 = f2 & g1 = g2 ) let f1, f2 be Function of X,D1; ::_thesis: for g1, g2 being Function of X,D2 st <:f1,g1:> = <:f2,g2:> holds ( f1 = f2 & g1 = g2 ) let g1, g2 be Function of X,D2; ::_thesis: ( <:f1,g1:> = <:f2,g2:> implies ( f1 = f2 & g1 = g2 ) ) A1: ( dom g1 = X & dom g2 = X ) by FUNCT_2:def_1; ( dom f1 = X & dom f2 = X ) by FUNCT_2:def_1; hence ( <:f1,g1:> = <:f2,g2:> implies ( f1 = f2 & g1 = g2 ) ) by A1, Th54; ::_thesis: verum end; definition let f, g be Function; func[:f,g:] -> Function means :Def8: :: FUNCT_3:def 8 ( dom it = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds it . (x,y) = [(f . x),(g . y)] ) ); existence ex b1 being Function st ( dom b1 = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds b1 . (x,y) = [(f . x),(g . y)] ) ) proof deffunc H1( set , set ) -> set = [(f . \$1),(g . \$2)]; ex F being Function st ( dom F = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds F . (x,y) = H1(x,y) ) ) from FUNCT_3:sch_2(); hence ex b1 being Function st ( dom b1 = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds b1 . (x,y) = [(f . x),(g . y)] ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds b1 . (x,y) = [(f . x),(g . y)] ) & dom b2 = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds b2 . (x,y) = [(f . x),(g . y)] ) holds b1 = b2 proof let fg1, fg2 be Function; ::_thesis: ( dom fg1 = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds fg1 . (x,y) = [(f . x),(g . y)] ) & dom fg2 = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds fg2 . (x,y) = [(f . x),(g . y)] ) implies fg1 = fg2 ) assume that A1: dom fg1 = [:(dom f),(dom g):] and A2: for x, y being set st x in dom f & y in dom g holds fg1 . (x,y) = [(f . x),(g . y)] and A3: dom fg2 = [:(dom f),(dom g):] and A4: for x, y being set st x in dom f & y in dom g holds fg2 . (x,y) = [(f . x),(g . y)] ; ::_thesis: fg1 = fg2 for p being set st p in [:(dom f),(dom g):] holds fg1 . p = fg2 . p proof let p be set ; ::_thesis: ( p in [:(dom f),(dom g):] implies fg1 . p = fg2 . p ) assume p in [:(dom f),(dom g):] ; ::_thesis: fg1 . p = fg2 . p then consider x, y being set such that A5: ( x in dom f & y in dom g ) and A6: p = [x,y] by ZFMISC_1:def_2; ( fg1 . (x,y) = [(f . x),(g . y)] & fg2 . (x,y) = [(f . x),(g . y)] ) by A2, A4, A5; hence fg1 . p = fg2 . p by A6; ::_thesis: verum end; hence fg1 = fg2 by A1, A3, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def8 defines [: FUNCT_3:def_8_:_ for f, g, b3 being Function holds ( b3 = [:f,g:] iff ( dom b3 = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds b3 . (x,y) = [(f . x),(g . y)] ) ) ); theorem Th65: :: FUNCT_3:65 for f, g being Function for x, y being set st [x,y] in [:(dom f),(dom g):] holds [:f,g:] . (x,y) = [(f . x),(g . y)] proof let f, g be Function; ::_thesis: for x, y being set st [x,y] in [:(dom f),(dom g):] holds [:f,g:] . (x,y) = [(f . x),(g . y)] let x, y be set ; ::_thesis: ( [x,y] in [:(dom f),(dom g):] implies [:f,g:] . (x,y) = [(f . x),(g . y)] ) assume [x,y] in [:(dom f),(dom g):] ; ::_thesis: [:f,g:] . (x,y) = [(f . x),(g . y)] then ( x in dom f & y in dom g ) by ZFMISC_1:87; hence [:f,g:] . (x,y) = [(f . x),(g . y)] by Def8; ::_thesis: verum end; theorem Th66: :: FUNCT_3:66 for f, g being Function holds [:f,g:] = <:(f * (pr1 ((dom f),(dom g)))),(g * (pr2 ((dom f),(dom g)))):> proof let f, g be Function; ::_thesis: [:f,g:] = <:(f * (pr1 ((dom f),(dom g)))),(g * (pr2 ((dom f),(dom g)))):> A1: dom (pr1 ((dom f),(dom g))) = [:(dom f),(dom g):] by Def4; A2: dom (pr2 ((dom f),(dom g))) = [:(dom f),(dom g):] by Def5; rng (pr2 ((dom f),(dom g))) c= dom g by Th45; then A3: dom (g * (pr2 ((dom f),(dom g)))) = [:(dom f),(dom g):] by A2, RELAT_1:27; rng (pr1 ((dom f),(dom g))) c= dom f by Th43; then dom (f * (pr1 ((dom f),(dom g)))) = [:(dom f),(dom g):] by A1, RELAT_1:27; then A4: dom <:(f * (pr1 ((dom f),(dom g)))),(g * (pr2 ((dom f),(dom g)))):> = [:(dom f),(dom g):] by A3, Th50; A5: for x, y being set st x in dom f & y in dom g holds [:f,g:] . (x,y) = <:(f * (pr1 ((dom f),(dom g)))),(g * (pr2 ((dom f),(dom g)))):> . (x,y) proof let x, y be set ; ::_thesis: ( x in dom f & y in dom g implies [:f,g:] . (x,y) = <:(f * (pr1 ((dom f),(dom g)))),(g * (pr2 ((dom f),(dom g)))):> . (x,y) ) assume A6: ( x in dom f & y in dom g ) ; ::_thesis: [:f,g:] . (x,y) = <:(f * (pr1 ((dom f),(dom g)))),(g * (pr2 ((dom f),(dom g)))):> . (x,y) then A7: [x,y] in [:(dom f),(dom g):] by ZFMISC_1:87; thus [:f,g:] . (x,y) = [(f . x),(g . y)] by A6, Def8 .= [(f . ((pr1 ((dom f),(dom g))) . (x,y))),(g . y)] by A6, Def4 .= [(f . ((pr1 ((dom f),(dom g))) . (x,y))),(g . ((pr2 ((dom f),(dom g))) . (x,y)))] by A6, Def5 .= [((f * (pr1 ((dom f),(dom g)))) . (x,y)),(g . ((pr2 ((dom f),(dom g))) . (x,y)))] by A1, A7, FUNCT_1:13 .= [((f * (pr1 ((dom f),(dom g)))) . (x,y)),((g * (pr2 ((dom f),(dom g)))) . (x,y))] by A2, A7, FUNCT_1:13 .= <:(f * (pr1 ((dom f),(dom g)))),(g * (pr2 ((dom f),(dom g)))):> . (x,y) by A4, A7, Def7 ; ::_thesis: verum end; dom [:f,g:] = [:(dom f),(dom g):] by Def8; hence [:f,g:] = <:(f * (pr1 ((dom f),(dom g)))),(g * (pr2 ((dom f),(dom g)))):> by A4, A5, Th6; ::_thesis: verum end; theorem Th67: :: FUNCT_3:67 for f, g being Function holds rng [:f,g:] = [:(rng f),(rng g):] proof let f, g be Function; ::_thesis: rng [:f,g:] = [:(rng f),(rng g):] for q being set holds ( q in rng [:f,g:] iff q in [:(rng f),(rng g):] ) proof let q be set ; ::_thesis: ( q in rng [:f,g:] iff q in [:(rng f),(rng g):] ) A1: dom [:f,g:] = [:(dom f),(dom g):] by Def8; thus ( q in rng [:f,g:] implies q in [:(rng f),(rng g):] ) ::_thesis: ( q in [:(rng f),(rng g):] implies q in rng [:f,g:] ) proof assume q in rng [:f,g:] ; ::_thesis: q in [:(rng f),(rng g):] then consider p being set such that A2: p in dom [:f,g:] and A3: q = [:f,g:] . p by FUNCT_1:def_3; p in [:(dom f),(dom g):] by A2, Def8; then consider x, y being set such that A4: ( x in dom f & y in dom g ) and A5: p = [x,y] by ZFMISC_1:def_2; A6: ( f . x in rng f & g . y in rng g ) by A4, FUNCT_1:def_3; q = [:f,g:] . (x,y) by A3, A5 .= [(f . x),(g . y)] by A4, Def8 ; hence q in [:(rng f),(rng g):] by A6, ZFMISC_1:87; ::_thesis: verum end; assume q in [:(rng f),(rng g):] ; ::_thesis: q in rng [:f,g:] then consider y1, y2 being set such that A7: y1 in rng f and A8: y2 in rng g and A9: q = [y1,y2] by ZFMISC_1:def_2; consider x2 being set such that A10: x2 in dom g and A11: y2 = g . x2 by A8, FUNCT_1:def_3; consider x1 being set such that A12: x1 in dom f and A13: y1 = f . x1 by A7, FUNCT_1:def_3; A14: [x1,x2] in [:(dom f),(dom g):] by A12, A10, ZFMISC_1:87; [:f,g:] . (x1,x2) = q by A9, A12, A13, A10, A11, Def8; hence q in rng [:f,g:] by A14, A1, FUNCT_1:def_3; ::_thesis: verum end; hence rng [:f,g:] = [:(rng f),(rng g):] by TARSKI:1; ::_thesis: verum end; theorem Th68: :: FUNCT_3:68 for X being set for f, g being Function st dom f = X & dom g = X holds <:f,g:> = [:f,g:] * (delta X) proof let X be set ; ::_thesis: for f, g being Function st dom f = X & dom g = X holds <:f,g:> = [:f,g:] * (delta X) let f, g be Function; ::_thesis: ( dom f = X & dom g = X implies <:f,g:> = [:f,g:] * (delta X) ) assume A1: ( dom f = X & dom g = X ) ; ::_thesis: <:f,g:> = [:f,g:] * (delta X) A2: dom (delta X) = X by Def6; rng (delta X) c= [:X,X:] by Th47; then rng (delta X) c= dom [:f,g:] by A1, Def8; then A3: dom ([:f,g:] * (delta X)) = X by A2, RELAT_1:27; (dom f) /\ (dom g) = X by A1; then A4: dom <:f,g:> = X by Def7; for x being set st x in X holds <:f,g:> . x = ([:f,g:] * (delta X)) . x proof let x be set ; ::_thesis: ( x in X implies <:f,g:> . x = ([:f,g:] * (delta X)) . x ) assume A5: x in X ; ::_thesis: <:f,g:> . x = ([:f,g:] * (delta X)) . x hence <:f,g:> . x = [(f . x),(g . x)] by A4, Def7 .= [:f,g:] . (x,x) by A1, A5, Def8 .= [:f,g:] . ((delta X) . x) by A5, Def6 .= ([:f,g:] * (delta X)) . x by A3, A5, FUNCT_1:12 ; ::_thesis: verum end; hence <:f,g:> = [:f,g:] * (delta X) by A4, A3, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCT_3:69 for X, Y being set holds [:(id X),(id Y):] = id [:X,Y:] proof let X, Y be set ; ::_thesis: [:(id X),(id Y):] = id [:X,Y:] rng (pr1 (X,Y)) c= X by Th43; then A1: (id X) * (pr1 (X,Y)) = pr1 (X,Y) by RELAT_1:53; rng (pr2 (X,Y)) c= Y by Th45; then A2: (id Y) * (pr2 (X,Y)) = pr2 (X,Y) by RELAT_1:53; ( dom (id X) = X & dom (id Y) = Y ) ; hence [:(id X),(id Y):] = <:(pr1 (X,Y)),(pr2 (X,Y)):> by A1, A2, Th66 .= id [:X,Y:] by Th53 ; ::_thesis: verum end; theorem :: FUNCT_3:70 for f, g, h, k being Function holds [:f,h:] * <:g,k:> = <:(f * g),(h * k):> proof let f, g, h, k be Function; ::_thesis: [:f,h:] * <:g,k:> = <:(f * g),(h * k):> for x being set holds ( x in dom ([:f,h:] * <:g,k:>) iff x in dom <:(f * g),(h * k):> ) proof let x be set ; ::_thesis: ( x in dom ([:f,h:] * <:g,k:>) iff x in dom <:(f * g),(h * k):> ) thus ( x in dom ([:f,h:] * <:g,k:>) implies x in dom <:(f * g),(h * k):> ) ::_thesis: ( x in dom <:(f * g),(h * k):> implies x in dom ([:f,h:] * <:g,k:>) ) proof assume A1: x in dom ([:f,h:] * <:g,k:>) ; ::_thesis: x in dom <:(f * g),(h * k):> then A2: x in dom <:g,k:> by FUNCT_1:11; then A3: x in (dom g) /\ (dom k) by Def7; then A4: x in dom g by XBOOLE_0:def_4; A5: x in dom k by A3, XBOOLE_0:def_4; <:g,k:> . x in dom [:f,h:] by A1, FUNCT_1:11; then [(g . x),(k . x)] in dom [:f,h:] by A2, Def7; then A6: [(g . x),(k . x)] in [:(dom f),(dom h):] by Def8; then k . x in dom h by ZFMISC_1:87; then A7: x in dom (h * k) by A5, FUNCT_1:11; g . x in dom f by A6, ZFMISC_1:87; then x in dom (f * g) by A4, FUNCT_1:11; then x in (dom (f * g)) /\ (dom (h * k)) by A7, XBOOLE_0:def_4; hence x in dom <:(f * g),(h * k):> by Def7; ::_thesis: verum end; assume x in dom <:(f * g),(h * k):> ; ::_thesis: x in dom ([:f,h:] * <:g,k:>) then A8: x in (dom (f * g)) /\ (dom (h * k)) by Def7; then A9: x in dom (f * g) by XBOOLE_0:def_4; A10: x in dom (h * k) by A8, XBOOLE_0:def_4; then A11: x in dom k by FUNCT_1:11; x in dom g by A9, FUNCT_1:11; then x in (dom g) /\ (dom k) by A11, XBOOLE_0:def_4; then A12: x in dom <:g,k:> by Def7; A13: k . x in dom h by A10, FUNCT_1:11; g . x in dom f by A9, FUNCT_1:11; then [(g . x),(k . x)] in [:(dom f),(dom h):] by A13, ZFMISC_1:87; then [(g . x),(k . x)] in dom [:f,h:] by Def8; then <:g,k:> . x in dom [:f,h:] by A12, Def7; hence x in dom ([:f,h:] * <:g,k:>) by A12, FUNCT_1:11; ::_thesis: verum end; then A14: dom ([:f,h:] * <:g,k:>) = dom <:(f * g),(h * k):> by TARSKI:1; for x being set st x in dom ([:f,h:] * <:g,k:>) holds ([:f,h:] * <:g,k:>) . x = <:(f * g),(h * k):> . x proof let x be set ; ::_thesis: ( x in dom ([:f,h:] * <:g,k:>) implies ([:f,h:] * <:g,k:>) . x = <:(f * g),(h * k):> . x ) assume A15: x in dom ([:f,h:] * <:g,k:>) ; ::_thesis: ([:f,h:] * <:g,k:>) . x = <:(f * g),(h * k):> . x then A16: x in dom <:g,k:> by FUNCT_1:11; then A17: x in (dom g) /\ (dom k) by Def7; then A18: x in dom g by XBOOLE_0:def_4; <:g,k:> . x in dom [:f,h:] by A15, FUNCT_1:11; then [(g . x),(k . x)] in dom [:f,h:] by A16, Def7; then A19: [(g . x),(k . x)] in [:(dom f),(dom h):] by Def8; then A20: g . x in dom f by ZFMISC_1:87; A21: x in dom k by A17, XBOOLE_0:def_4; A22: k . x in dom h by A19, ZFMISC_1:87; then A23: x in dom (h * k) by A21, FUNCT_1:11; x in dom (f * g) by A20, A18, FUNCT_1:11; then A24: x in (dom (f * g)) /\ (dom (h * k)) by A23, XBOOLE_0:def_4; thus ([:f,h:] * <:g,k:>) . x = [:f,h:] . (<:g,k:> . x) by A15, FUNCT_1:12 .= [:f,h:] . ((g . x),(k . x)) by A16, Def7 .= [(f . (g . x)),(h . (k . x))] by A20, A22, Def8 .= [((f * g) . x),(h . (k . x))] by A18, FUNCT_1:13 .= [((f * g) . x),((h * k) . x)] by A21, FUNCT_1:13 .= <:(f * g),(h * k):> . x by A24, Th48 ; ::_thesis: verum end; hence [:f,h:] * <:g,k:> = <:(f * g),(h * k):> by A14, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCT_3:71 for f, g, h, k being Function holds [:f,h:] * [:g,k:] = [:(f * g),(h * k):] proof let f, g, h, k be Function; ::_thesis: [:f,h:] * [:g,k:] = [:(f * g),(h * k):] A1: for x, y being set st x in dom (f * g) & y in dom (h * k) holds ([:f,h:] * [:g,k:]) . (x,y) = [:(f * g),(h * k):] . (x,y) proof let x, y be set ; ::_thesis: ( x in dom (f * g) & y in dom (h * k) implies ([:f,h:] * [:g,k:]) . (x,y) = [:(f * g),(h * k):] . (x,y) ) assume that A2: x in dom (f * g) and A3: y in dom (h * k) ; ::_thesis: ([:f,h:] * [:g,k:]) . (x,y) = [:(f * g),(h * k):] . (x,y) A4: ( g . x in dom f & k . y in dom h ) by A2, A3, FUNCT_1:11; A5: ( x in dom g & y in dom k ) by A2, A3, FUNCT_1:11; then [x,y] in [:(dom g),(dom k):] by ZFMISC_1:87; then [x,y] in dom [:g,k:] by Def8; hence ([:f,h:] * [:g,k:]) . (x,y) = [:f,h:] . ([:g,k:] . (x,y)) by FUNCT_1:13 .= [:f,h:] . ((g . x),(k . y)) by A5, Def8 .= [(f . (g . x)),(h . (k . y))] by A4, Def8 .= [((f * g) . x),(h . (k . y))] by A2, FUNCT_1:12 .= [((f * g) . x),((h * k) . y)] by A3, FUNCT_1:12 .= [:(f * g),(h * k):] . (x,y) by A2, A3, Def8 ; ::_thesis: verum end; for p being set holds ( p in dom ([:f,h:] * [:g,k:]) iff p in [:(dom (f * g)),(dom (h * k)):] ) proof let p be set ; ::_thesis: ( p in dom ([:f,h:] * [:g,k:]) iff p in [:(dom (f * g)),(dom (h * k)):] ) A6: dom [:g,k:] = [:(dom g),(dom k):] by Def8; A7: dom [:f,h:] = [:(dom f),(dom h):] by Def8; thus ( p in dom ([:f,h:] * [:g,k:]) implies p in [:(dom (f * g)),(dom (h * k)):] ) ::_thesis: ( p in [:(dom (f * g)),(dom (h * k)):] implies p in dom ([:f,h:] * [:g,k:]) ) proof assume A8: p in dom ([:f,h:] * [:g,k:]) ; ::_thesis: p in [:(dom (f * g)),(dom (h * k)):] then A9: [:g,k:] . p in dom [:f,h:] by FUNCT_1:11; A10: p in dom [:g,k:] by A8, FUNCT_1:11; then consider x1, x2 being set such that A11: x1 in dom g and A12: x2 in dom k and A13: p = [x1,x2] by A6, ZFMISC_1:def_2; [:g,k:] . (x1,x2) = [:g,k:] . p by A13; then A14: [(g . x1),(k . x2)] in dom [:f,h:] by A6, A10, A9, A13, Th65; then k . x2 in dom h by A7, ZFMISC_1:87; then A15: x2 in dom (h * k) by A12, FUNCT_1:11; g . x1 in dom f by A7, A14, ZFMISC_1:87; then x1 in dom (f * g) by A11, FUNCT_1:11; hence p in [:(dom (f * g)),(dom (h * k)):] by A13, A15, ZFMISC_1:87; ::_thesis: verum end; assume p in [:(dom (f * g)),(dom (h * k)):] ; ::_thesis: p in dom ([:f,h:] * [:g,k:]) then consider x1, x2 being set such that A16: ( x1 in dom (f * g) & x2 in dom (h * k) ) and A17: p = [x1,x2] by ZFMISC_1:def_2; ( x1 in dom g & x2 in dom k ) by A16, FUNCT_1:11; then A18: [x1,x2] in dom [:g,k:] by A6, ZFMISC_1:87; ( g . x1 in dom f & k . x2 in dom h ) by A16, FUNCT_1:11; then [(g . x1),(k . x2)] in dom [:f,h:] by A7, ZFMISC_1:87; then [:g,k:] . (x1,x2) in dom [:f,h:] by A6, A18, Th65; hence p in dom ([:f,h:] * [:g,k:]) by A17, A18, FUNCT_1:11; ::_thesis: verum end; then A19: dom ([:f,h:] * [:g,k:]) = [:(dom (f * g)),(dom (h * k)):] by TARSKI:1; [:(dom (f * g)),(dom (h * k)):] = dom [:(f * g),(h * k):] by Def8; hence [:f,h:] * [:g,k:] = [:(f * g),(h * k):] by A19, A1, Th6; ::_thesis: verum end; theorem :: FUNCT_3:72 for B, A being set for f, g being Function holds [:f,g:] .: [:B,A:] = [:(f .: B),(g .: A):] proof let B, A be set ; ::_thesis: for f, g being Function holds [:f,g:] .: [:B,A:] = [:(f .: B),(g .: A):] let f, g be Function; ::_thesis: [:f,g:] .: [:B,A:] = [:(f .: B),(g .: A):] for q being set holds ( q in [:f,g:] .: [:B,A:] iff q in [:(f .: B),(g .: A):] ) proof let q be set ; ::_thesis: ( q in [:f,g:] .: [:B,A:] iff q in [:(f .: B),(g .: A):] ) A1: [:(dom f),(dom g):] = dom [:f,g:] by Def8; thus ( q in [:f,g:] .: [:B,A:] implies q in [:(f .: B),(g .: A):] ) ::_thesis: ( q in [:(f .: B),(g .: A):] implies q in [:f,g:] .: [:B,A:] ) proof assume q in [:f,g:] .: [:B,A:] ; ::_thesis: q in [:(f .: B),(g .: A):] then consider p being set such that A2: p in dom [:f,g:] and A3: p in [:B,A:] and A4: q = [:f,g:] . p by FUNCT_1:def_6; dom [:f,g:] = [:(dom f),(dom g):] by Def8; then consider x, y being set such that A5: x in dom f and A6: y in dom g and A7: p = [x,y] by A2, ZFMISC_1:def_2; x in B by A3, A7, ZFMISC_1:87; then A8: f . x in f .: B by A5, FUNCT_1:def_6; y in A by A3, A7, ZFMISC_1:87; then A9: g . y in g .: A by A6, FUNCT_1:def_6; q = [:f,g:] . (x,y) by A4, A7; then q = [(f . x),(g . y)] by A5, A6, Def8; hence q in [:(f .: B),(g .: A):] by A8, A9, ZFMISC_1:87; ::_thesis: verum end; assume q in [:(f .: B),(g .: A):] ; ::_thesis: q in [:f,g:] .: [:B,A:] then consider y1, y2 being set such that A10: y1 in f .: B and A11: y2 in g .: A and A12: q = [y1,y2] by ZFMISC_1:def_2; consider x1 being set such that A13: x1 in dom f and A14: x1 in B and A15: y1 = f . x1 by A10, FUNCT_1:def_6; consider x2 being set such that A16: x2 in dom g and A17: x2 in A and A18: y2 = g . x2 by A11, FUNCT_1:def_6; A19: [:f,g:] . (x1,x2) = [(f . x1),(g . x2)] by A13, A16, Def8; ( [x1,x2] in [:(dom f),(dom g):] & [x1,x2] in [:B,A:] ) by A13, A14, A16, A17, ZFMISC_1:87; hence q in [:f,g:] .: [:B,A:] by A12, A15, A18, A1, A19, FUNCT_1:def_6; ::_thesis: verum end; hence [:f,g:] .: [:B,A:] = [:(f .: B),(g .: A):] by TARSKI:1; ::_thesis: verum end; theorem :: FUNCT_3:73 for B, A being set for f, g being Function holds [:f,g:] " [:B,A:] = [:(f " B),(g " A):] proof let B, A be set ; ::_thesis: for f, g being Function holds [:f,g:] " [:B,A:] = [:(f " B),(g " A):] let f, g be Function; ::_thesis: [:f,g:] " [:B,A:] = [:(f " B),(g " A):] for q being set holds ( q in [:f,g:] " [:B,A:] iff q in [:(f " B),(g " A):] ) proof let q be set ; ::_thesis: ( q in [:f,g:] " [:B,A:] iff q in [:(f " B),(g " A):] ) thus ( q in [:f,g:] " [:B,A:] implies q in [:(f " B),(g " A):] ) ::_thesis: ( q in [:(f " B),(g " A):] implies q in [:f,g:] " [:B,A:] ) proof assume A1: q in [:f,g:] " [:B,A:] ; ::_thesis: q in [:(f " B),(g " A):] then A2: [:f,g:] . q in [:B,A:] by FUNCT_1:def_7; q in dom [:f,g:] by A1, FUNCT_1:def_7; then q in [:(dom f),(dom g):] by Def8; then consider x1, x2 being set such that A3: x1 in dom f and A4: x2 in dom g and A5: q = [x1,x2] by ZFMISC_1:def_2; [:f,g:] . q = [:f,g:] . (x1,x2) by A5; then A6: [(f . x1),(g . x2)] in [:B,A:] by A3, A4, A2, Def8; then g . x2 in A by ZFMISC_1:87; then A7: x2 in g " A by A4, FUNCT_1:def_7; f . x1 in B by A6, ZFMISC_1:87; then x1 in f " B by A3, FUNCT_1:def_7; hence q in [:(f " B),(g " A):] by A5, A7, ZFMISC_1:87; ::_thesis: verum end; assume q in [:(f " B),(g " A):] ; ::_thesis: q in [:f,g:] " [:B,A:] then consider x1, x2 being set such that A8: ( x1 in f " B & x2 in g " A ) and A9: q = [x1,x2] by ZFMISC_1:def_2; ( f . x1 in B & g . x2 in A ) by A8, FUNCT_1:def_7; then A10: [(f . x1),(g . x2)] in [:B,A:] by ZFMISC_1:87; ( x1 in dom f & x2 in dom g ) by A8, FUNCT_1:def_7; then A11: ( [x1,x2] in [:(dom f),(dom g):] & [:f,g:] . (x1,x2) = [(f . x1),(g . x2)] ) by Def8, ZFMISC_1:87; [:(dom f),(dom g):] = dom [:f,g:] by Def8; hence q in [:f,g:] " [:B,A:] by A9, A11, A10, FUNCT_1:def_7; ::_thesis: verum end; hence [:f,g:] " [:B,A:] = [:(f " B),(g " A):] by TARSKI:1; ::_thesis: verum end; theorem Th74: :: FUNCT_3:74 for X, Y, V, Z being set for f being Function of X,Y for g being Function of V,Z holds [:f,g:] is Function of [:X,V:],[:Y,Z:] proof let X, Y, V, Z be set ; ::_thesis: for f being Function of X,Y for g being Function of V,Z holds [:f,g:] is Function of [:X,V:],[:Y,Z:] let f be Function of X,Y; ::_thesis: for g being Function of V,Z holds [:f,g:] is Function of [:X,V:],[:Y,Z:] let g be Function of V,Z; ::_thesis: [:f,g:] is Function of [:X,V:],[:Y,Z:] percases not ( [:Y,Z:] = {} & not [:X,V:] = {} & not ( [:Y,Z:] = {} & [:X,V:] <> {} ) ) ; supposeA1: ( [:Y,Z:] = {} implies [:X,V:] = {} ) ; ::_thesis: [:f,g:] is Function of [:X,V:],[:Y,Z:] now__::_thesis:_[:f,g:]_is_Function_of_[:X,V:],[:Y,Z:] percases ( [:Y,Z:] <> {} or [:X,V:] = {} ) by A1; supposeA2: [:Y,Z:] <> {} ; ::_thesis: [:f,g:] is Function of [:X,V:],[:Y,Z:] ( rng f c= Y & rng g c= Z ) by RELAT_1:def_19; then [:(rng f),(rng g):] c= [:Y,Z:] by ZFMISC_1:96; then A3: rng [:f,g:] c= [:Y,Z:] by Th67; ( Z = {} implies V = {} ) by A2, ZFMISC_1:90; then A4: dom g = V by FUNCT_2:def_1; ( Y = {} implies X = {} ) by A2, ZFMISC_1:90; then dom f = X by FUNCT_2:def_1; then dom [:f,g:] = [:X,V:] by A4, Def8; hence [:f,g:] is Function of [:X,V:],[:Y,Z:] by A3, FUNCT_2:2; ::_thesis: verum end; supposeA5: [:X,V:] = {} ; ::_thesis: [:f,g:] is Function of [:X,V:],[:Y,Z:] then ( X = {} or V = {} ) ; then ( dom f = {} or dom g = {} ) ; then [:(dom f),(dom g):] = {} by ZFMISC_1:90; then A6: dom [:f,g:] = [:X,V:] by A5, Def8; ( rng f c= Y & rng g c= Z ) by RELAT_1:def_19; then [:(rng f),(rng g):] c= [:Y,Z:] by ZFMISC_1:96; then rng [:f,g:] c= [:Y,Z:] by Th67; hence [:f,g:] is Function of [:X,V:],[:Y,Z:] by A6, FUNCT_2:2; ::_thesis: verum end; end; end; hence [:f,g:] is Function of [:X,V:],[:Y,Z:] ; ::_thesis: verum end; supposeA7: ( [:Y,Z:] = {} & [:X,V:] <> {} ) ; ::_thesis: [:f,g:] is Function of [:X,V:],[:Y,Z:] then ( Y = {} or Z = {} ) ; then ( f = {} or g = {} ) ; then [:(dom f),(dom g):] = {} by RELAT_1:38, ZFMISC_1:90; then A8: dom [:f,g:] = {} by Def8; then ( rng [:f,g:] = {} & dom [:f,g:] c= [:X,V:] ) by RELAT_1:42, XBOOLE_1:2; then reconsider R = [:f,g:] as Relation of [:X,V:],[:Y,Z:] by RELSET_1:4, XBOOLE_1:2; [:f,g:] = {} by A8; then R is quasi_total by A7, FUNCT_2:def_1; hence [:f,g:] is Function of [:X,V:],[:Y,Z:] ; ::_thesis: verum end; end; end; definition let X1, X2, Y1, Y2 be set ; let f1 be Function of X1,Y1; let f2 be Function of X2,Y2; :: original: [: redefine func[:f1,f2:] -> Function of [:X1,X2:],[:Y1,Y2:]; coherence [:f1,f2:] is Function of [:X1,X2:],[:Y1,Y2:] by Th74; end; theorem :: FUNCT_3:75 for C1, D1, C2, D2 being non empty set for f1 being Function of C1,D1 for f2 being Function of C2,D2 for c1 being Element of C1 for c2 being Element of C2 holds [:f1,f2:] . (c1,c2) = [(f1 . c1),(f2 . c2)] proof let C1, D1, C2, D2 be non empty set ; ::_thesis: for f1 being Function of C1,D1 for f2 being Function of C2,D2 for c1 being Element of C1 for c2 being Element of C2 holds [:f1,f2:] . (c1,c2) = [(f1 . c1),(f2 . c2)] let f1 be Function of C1,D1; ::_thesis: for f2 being Function of C2,D2 for c1 being Element of C1 for c2 being Element of C2 holds [:f1,f2:] . (c1,c2) = [(f1 . c1),(f2 . c2)] let f2 be Function of C2,D2; ::_thesis: for c1 being Element of C1 for c2 being Element of C2 holds [:f1,f2:] . (c1,c2) = [(f1 . c1),(f2 . c2)] let c1 be Element of C1; ::_thesis: for c2 being Element of C2 holds [:f1,f2:] . (c1,c2) = [(f1 . c1),(f2 . c2)] let c2 be Element of C2; ::_thesis: [:f1,f2:] . (c1,c2) = [(f1 . c1),(f2 . c2)] ( dom f1 = C1 & dom f2 = C2 ) by FUNCT_2:def_1; hence [:f1,f2:] . (c1,c2) = [(f1 . c1),(f2 . c2)] by Def8; ::_thesis: verum end; theorem :: FUNCT_3:76 for X1, Y1, X2, Y2 being set for f1 being Function of X1,Y1 for f2 being Function of X2,Y2 st ( Y1 = {} implies X1 = {} ) & ( Y2 = {} implies X2 = {} ) holds [:f1,f2:] = <:(f1 * (pr1 (X1,X2))),(f2 * (pr2 (X1,X2))):> proof let X1, Y1, X2, Y2 be set ; ::_thesis: for f1 being Function of X1,Y1 for f2 being Function of X2,Y2 st ( Y1 = {} implies X1 = {} ) & ( Y2 = {} implies X2 = {} ) holds [:f1,f2:] = <:(f1 * (pr1 (X1,X2))),(f2 * (pr2 (X1,X2))):> let f1 be Function of X1,Y1; ::_thesis: for f2 being Function of X2,Y2 st ( Y1 = {} implies X1 = {} ) & ( Y2 = {} implies X2 = {} ) holds [:f1,f2:] = <:(f1 * (pr1 (X1,X2))),(f2 * (pr2 (X1,X2))):> let f2 be Function of X2,Y2; ::_thesis: ( ( Y1 = {} implies X1 = {} ) & ( Y2 = {} implies X2 = {} ) implies [:f1,f2:] = <:(f1 * (pr1 (X1,X2))),(f2 * (pr2 (X1,X2))):> ) assume ( ( Y1 = {} implies X1 = {} ) & ( Y2 = {} implies X2 = {} ) ) ; ::_thesis: [:f1,f2:] = <:(f1 * (pr1 (X1,X2))),(f2 * (pr2 (X1,X2))):> then ( dom f1 = X1 & dom f2 = X2 ) by FUNCT_2:def_1; hence [:f1,f2:] = <:(f1 * (pr1 (X1,X2))),(f2 * (pr2 (X1,X2))):> by Th66; ::_thesis: verum end; theorem :: FUNCT_3:77 for X1, X2 being set for D1, D2 being non empty set for f1 being Function of X1,D1 for f2 being Function of X2,D2 holds [:f1,f2:] = <:(f1 * (pr1 (X1,X2))),(f2 * (pr2 (X1,X2))):> proof let X1, X2 be set ; ::_thesis: for D1, D2 being non empty set for f1 being Function of X1,D1 for f2 being Function of X2,D2 holds [:f1,f2:] = <:(f1 * (pr1 (X1,X2))),(f2 * (pr2 (X1,X2))):> let D1, D2 be non empty set ; ::_thesis: for f1 being Function of X1,D1 for f2 being Function of X2,D2 holds [:f1,f2:] = <:(f1 * (pr1 (X1,X2))),(f2 * (pr2 (X1,X2))):> let f1 be Function of X1,D1; ::_thesis: for f2 being Function of X2,D2 holds [:f1,f2:] = <:(f1 * (pr1 (X1,X2))),(f2 * (pr2 (X1,X2))):> let f2 be Function of X2,D2; ::_thesis: [:f1,f2:] = <:(f1 * (pr1 (X1,X2))),(f2 * (pr2 (X1,X2))):> ( dom f1 = X1 & dom f2 = X2 ) by FUNCT_2:def_1; hence [:f1,f2:] = <:(f1 * (pr1 (X1,X2))),(f2 * (pr2 (X1,X2))):> by Th66; ::_thesis: verum end; theorem :: FUNCT_3:78 for X, Y1, Y2 being set for f1 being Function of X,Y1 for f2 being Function of X,Y2 holds <:f1,f2:> = [:f1,f2:] * (delta X) proof let X, Y1, Y2 be set ; ::_thesis: for f1 being Function of X,Y1 for f2 being Function of X,Y2 holds <:f1,f2:> = [:f1,f2:] * (delta X) let f1 be Function of X,Y1; ::_thesis: for f2 being Function of X,Y2 holds <:f1,f2:> = [:f1,f2:] * (delta X) let f2 be Function of X,Y2; ::_thesis: <:f1,f2:> = [:f1,f2:] * (delta X) percases ( Y1 = {} or Y2 = {} or ( Y1 <> {} & Y2 <> {} ) ) ; suppose ( Y1 = {} or Y2 = {} ) ; ::_thesis: <:f1,f2:> = [:f1,f2:] * (delta X) then A1: ( dom f1 = {} or dom f2 = {} ) ; A2: dom [:f1,f2:] = [:(dom f1),(dom f2):] by Def8 .= {} by A1, ZFMISC_1:90 ; dom <:f1,f2:> = (dom f1) /\ (dom f2) by Def7 .= {} by A1 ; hence <:f1,f2:> = {} * (delta X) .= [:f1,f2:] * (delta X) by A2, RELAT_1:41 ; ::_thesis: verum end; suppose ( Y1 <> {} & Y2 <> {} ) ; ::_thesis: <:f1,f2:> = [:f1,f2:] * (delta X) then ( dom f1 = X & dom f2 = X ) by FUNCT_2:def_1; hence <:f1,f2:> = [:f1,f2:] * (delta X) by Th68; ::_thesis: verum end; end; end; begin theorem :: FUNCT_3:79 for f being Function holds (pr1 ((dom f),(rng f))) .: f = dom f proof let f be Function; ::_thesis: (pr1 ((dom f),(rng f))) .: f = dom f now__::_thesis:_for_y_being_set_holds_ (_(_y_in_dom_f_implies_ex_x_being_set_st_ (_x_in_dom_(pr1_((dom_f),(rng_f)))_&_x_in_f_&_y_=_(pr1_((dom_f),(rng_f)))_._x_)_)_&_(_ex_x_being_set_st_ (_x_in_dom_(pr1_((dom_f),(rng_f)))_&_x_in_f_&_y_=_(pr1_((dom_f),(rng_f)))_._x_)_implies_y_in_dom_f_)_) let y be set ; ::_thesis: ( ( y in dom f implies ex x being set st ( x in dom (pr1 ((dom f),(rng f))) & x in f & y = (pr1 ((dom f),(rng f))) . x ) ) & ( ex x being set st ( x in dom (pr1 ((dom f),(rng f))) & x in f & y = (pr1 ((dom f),(rng f))) . x ) implies y in dom f ) ) thus ( y in dom f implies ex x being set st ( x in dom (pr1 ((dom f),(rng f))) & x in f & y = (pr1 ((dom f),(rng f))) . x ) ) ::_thesis: ( ex x being set st ( x in dom (pr1 ((dom f),(rng f))) & x in f & y = (pr1 ((dom f),(rng f))) . x ) implies y in dom f ) proof assume A1: y in dom f ; ::_thesis: ex x being set st ( x in dom (pr1 ((dom f),(rng f))) & x in f & y = (pr1 ((dom f),(rng f))) . x ) take [y,(f . y)] ; ::_thesis: ( [y,(f . y)] in dom (pr1 ((dom f),(rng f))) & [y,(f . y)] in f & y = (pr1 ((dom f),(rng f))) . [y,(f . y)] ) A2: f . y in rng f by A1, FUNCT_1:def_3; then [y,(f . y)] in [:(dom f),(rng f):] by A1, ZFMISC_1:87; hence [y,(f . y)] in dom (pr1 ((dom f),(rng f))) by Def4; ::_thesis: ( [y,(f . y)] in f & y = (pr1 ((dom f),(rng f))) . [y,(f . y)] ) thus [y,(f . y)] in f by A1, FUNCT_1:def_2; ::_thesis: y = (pr1 ((dom f),(rng f))) . [y,(f . y)] thus y = (pr1 ((dom f),(rng f))) . (y,(f . y)) by A1, A2, Def4 .= (pr1 ((dom f),(rng f))) . [y,(f . y)] ; ::_thesis: verum end; given x being set such that A3: x in dom (pr1 ((dom f),(rng f))) and x in f and A4: y = (pr1 ((dom f),(rng f))) . x ; ::_thesis: y in dom f consider x1, x2 being set such that A5: ( x1 in dom f & x2 in rng f ) and A6: x = [x1,x2] by A3, ZFMISC_1:84; y = (pr1 ((dom f),(rng f))) . (x1,x2) by A4, A6; hence y in dom f by A5, Def4; ::_thesis: verum end; hence (pr1 ((dom f),(rng f))) .: f = dom f by FUNCT_1:def_6; ::_thesis: verum end; theorem :: FUNCT_3:80 for A, B, C being non empty set for f, g being Function of A,[:B,C:] st (pr1 (B,C)) * f = (pr1 (B,C)) * g & (pr2 (B,C)) * f = (pr2 (B,C)) * g holds f = g proof let A, B, C be non empty set ; ::_thesis: for f, g being Function of A,[:B,C:] st (pr1 (B,C)) * f = (pr1 (B,C)) * g & (pr2 (B,C)) * f = (pr2 (B,C)) * g holds f = g let f, g be Function of A,[:B,C:]; ::_thesis: ( (pr1 (B,C)) * f = (pr1 (B,C)) * g & (pr2 (B,C)) * f = (pr2 (B,C)) * g implies f = g ) assume A1: ( (pr1 (B,C)) * f = (pr1 (B,C)) * g & (pr2 (B,C)) * f = (pr2 (B,C)) * g ) ; ::_thesis: f = g now__::_thesis:_for_a_being_Element_of_A_holds_f_._a_=_g_._a let a be Element of A; ::_thesis: f . a = g . a consider b1 being Element of B, c1 being Element of C such that A2: f . a = [b1,c1] by DOMAIN_1:1; consider b2 being Element of B, c2 being Element of C such that A3: g . a = [b2,c2] by DOMAIN_1:1; A4: (pr1 (B,C)) . (g . a) = ((pr1 (B,C)) * g) . a by FUNCT_2:15; A5: ( (pr1 (B,C)) . (f . a) = ((pr1 (B,C)) * f) . a & (pr2 (B,C)) . (f . a) = ((pr2 (B,C)) * f) . a ) by FUNCT_2:15; A6: ( (pr2 (B,C)) . (b1,c1) = c1 & (pr2 (B,C)) . (b2,c2) = c2 ) by Def5; ( (pr1 (B,C)) . (b1,c1) = b1 & (pr1 (B,C)) . (b2,c2) = b2 ) by Def4; hence f . a = g . a by A1, A2, A3, A6, A5, A4, FUNCT_2:15; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; registration let F, G be one-to-one Function; cluster[:F,G:] -> one-to-one ; coherence [:F,G:] is one-to-one proof let z1, z2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not z1 in dom [:F,G:] or not z2 in dom [:F,G:] or not [:F,G:] . z1 = [:F,G:] . z2 or z1 = z2 ) assume that A1: z1 in dom [:F,G:] and A2: z2 in dom [:F,G:] and A3: [:F,G:] . z1 = [:F,G:] . z2 ; ::_thesis: z1 = z2 A4: dom [:F,G:] = [:(dom F),(dom G):] by Def8; then consider x1, y1 being set such that A5: x1 in dom F and A6: y1 in dom G and A7: z1 = [x1,y1] by A1, ZFMISC_1:84; A8: [:F,G:] . (x1,y1) = [(F . x1),(G . y1)] by A5, A6, Def8; consider x2, y2 being set such that A9: x2 in dom F and A10: y2 in dom G and A11: z2 = [x2,y2] by A2, A4, ZFMISC_1:84; A12: [:F,G:] . (x2,y2) = [(F . x2),(G . y2)] by A9, A10, Def8; then F . x1 = F . x2 by A3, A7, A11, A8, XTUPLE_0:1; then A13: x1 = x2 by A5, A9, FUNCT_1:def_4; G . y1 = G . y2 by A3, A7, A11, A8, A12, XTUPLE_0:1; hence z1 = z2 by A6, A7, A10, A11, A13, FUNCT_1:def_4; ::_thesis: verum end; end; registration let A be set ; cluster Relation-like [:A,A:] -defined A -valued Function-like quasi_total idempotent for Element of bool [:[:A,A:],A:]; existence ex b1 being BinOp of A st b1 is idempotent proof take pr1 (A,A) ; ::_thesis: pr1 (A,A) is idempotent percases ( A <> {} or A = {} ) ; supposeA1: A <> {} ; ::_thesis: pr1 (A,A) is idempotent let a be Element of A; :: according to BINOP_1:def_4 ::_thesis: (pr1 (A,A)) . (a,a) = a a in A by A1; hence (pr1 (A,A)) . (a,a) = a by Def4; ::_thesis: verum end; supposeA2: A = {} ; ::_thesis: pr1 (A,A) is idempotent let a be Element of A; :: according to BINOP_1:def_4 ::_thesis: (pr1 (A,A)) . (a,a) = a not [a,a] in dom (pr1 (A,A)) by A2; hence (pr1 (A,A)) . (a,a) = {} by FUNCT_1:def_2 .= a by A2, SUBSET_1:def_1 ; ::_thesis: verum end; end; end; end; registration let A be set ; let b be idempotent BinOp of A; let a be Element of A; reduceb . (a,a) to a; reducibility b . (a,a) = a by BINOP_1:def_4; end;