:: 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;