:: by Czes{\l}aw Byli\'nski

::

:: Received May 9, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

:: Additional propositions about functions

scheme :: FUNCT_3:sch 1

FuncEx3{ F_{1}() -> set , F_{2}() -> set , P_{1}[ set , set , set ] } :

FuncEx3{ F

ex f being Function st

( dom f = [:F_{1}(),F_{2}():] & ( for x, y being set st x in F_{1}() & y in F_{2}() holds

P_{1}[x,y,f . (x,y)] ) )

provided( dom f = [:F

P

A1:
for x, y, z1, z2 being set st x in F_{1}() & y in F_{2}() & P_{1}[x,y,z1] & P_{1}[x,y,z2] holds

z1 = z2 and

A2: for x, y being set st x in F_{1}() & y in F_{2}() holds

ex z being set st P_{1}[x,y,z]

z1 = z2 and

A2: for x, y being set st x in F

ex z being set st P

proof 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

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

:: Function indicated by the image under a function

definition

let f be Function;

ex b_{1} being Function st

( dom b_{1} = bool (dom f) & ( for X being set st X c= dom f holds

b_{1} . X = f .: X ) )

for b_{1}, b_{2} being Function st dom b_{1} = bool (dom f) & ( for X being set st X c= dom f holds

b_{1} . X = f .: X ) & dom b_{2} = bool (dom f) & ( for X being set st X c= dom f holds

b_{2} . X = f .: X ) holds

b_{1} = b_{2}

end;
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 ( dom it = bool (dom f) & ( for X being set st X c= dom f holds

it . X = f .: X ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines .: FUNCT_3:def 1 :

for f, b_{2} being Function holds

( b_{2} = .: f iff ( dom b_{2} = bool (dom f) & ( for X being set st X c= dom f holds

b_{2} . X = f .: X ) ) );

for f, b

( b

b

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)

for f being Function st A c= bool (dom f) holds

f .: (union A) = union ((.: f) .: A)

proof 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)

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 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)

for f being Function of X,Y st ( Y = {} implies X = {} ) holds

.: f is Function of (bool X),(bool Y)

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

:: Function indicated by the inverse image under a function

definition

let f be Function;

ex b_{1} being Function st

( dom b_{1} = bool (rng f) & ( for Y being set st Y c= rng f holds

b_{1} . Y = f " Y ) )

for b_{1}, b_{2} being Function st dom b_{1} = bool (rng f) & ( for Y being set st Y c= rng f holds

b_{1} . Y = f " Y ) & dom b_{2} = bool (rng f) & ( for Y being set st Y c= rng f holds

b_{2} . Y = f " Y ) holds

b_{1} = b_{2}

end;
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 ( dom it = bool (rng f) & ( for Y being set st Y c= rng f holds

it . Y = f " Y ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines " FUNCT_3:def 2 :

for f, b_{2} being Function holds

( b_{2} = " f iff ( dom b_{2} = bool (rng f) & ( for Y being set st Y c= rng f holds

b_{2} . Y = f " Y ) ) );

for f, b

( b

b

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)

for f being Function st A c= bool (dom f) & f is one-to-one holds

union ((" f) " A) = f .: (union A)

proof 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

for A being set st f is one-to-one & A c= bool (dom f) holds

(" f) " A = (.: f) .: A

proof end;

:: Characteristic function

definition

let A, X be set ;

ex b_{1} being Function st

( dom b_{1} = X & ( for x being set st x in X holds

( ( x in A implies b_{1} . x = 1 ) & ( not x in A implies b_{1} . x = {} ) ) ) )

for b_{1}, b_{2} being Function st dom b_{1} = X & ( for x being set st x in X holds

( ( x in A implies b_{1} . x = 1 ) & ( not x in A implies b_{1} . x = {} ) ) ) & dom b_{2} = X & ( for x being set st x in X holds

( ( x in A implies b_{2} . x = 1 ) & ( not x in A implies b_{2} . x = {} ) ) ) holds

b_{1} = b_{2}

end;
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 ( 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 = {} ) ) ) );

ex b

( dom b

( ( x in A implies b

proof end;

uniqueness for b

( ( x in A implies b

( ( x in A implies b

b

proof end;

:: deftheorem Def3 defines chi FUNCT_3:def 3 :

for A, X being set

for b_{3} being Function holds

( b_{3} = chi (A,X) iff ( dom b_{3} = X & ( for x being set st x in X holds

( ( x in A implies b_{3} . x = 1 ) & ( not x in A implies b_{3} . x = {} ) ) ) ) );

for A, X being set

for b

( b

( ( x in A implies b

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}

end;
:: original: chi

redefine func chi (A,X) -> Function of X,{{},1};

coherence

chi (A,X) is Function of X,{{},1}

proof 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

end;
let A be Subset of Y;

:: original: incl

redefine func incl A -> Function of A,Y;

coherence

incl is Function of A,Y

proof end;

:: Projections

definition

let X, Y be set ;

ex b_{1} being Function st

( dom b_{1} = [:X,Y:] & ( for x, y being set st x in X & y in Y holds

b_{1} . (x,y) = x ) )

for b_{1}, b_{2} being Function st dom b_{1} = [:X,Y:] & ( for x, y being set st x in X & y in Y holds

b_{1} . (x,y) = x ) & dom b_{2} = [:X,Y:] & ( for x, y being set st x in X & y in Y holds

b_{2} . (x,y) = x ) holds

b_{1} = b_{2}

ex b_{1} being Function st

( dom b_{1} = [:X,Y:] & ( for x, y being set st x in X & y in Y holds

b_{1} . (x,y) = y ) )

for b_{1}, b_{2} being Function st dom b_{1} = [:X,Y:] & ( for x, y being set st x in X & y in Y holds

b_{1} . (x,y) = y ) & dom b_{2} = [:X,Y:] & ( for x, y being set st x in X & y in Y holds

b_{2} . (x,y) = y ) holds

b_{1} = b_{2}

end;
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 ( dom it = [:X,Y:] & ( for x, y being set st x in X & y in Y holds

it . (x,y) = x ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 ( dom it = [:X,Y:] & ( for x, y being set st x in X & y in Y holds

it . (x,y) = y ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines pr1 FUNCT_3:def 4 :

for X, Y being set

for b_{3} being Function holds

( b_{3} = pr1 (X,Y) iff ( dom b_{3} = [:X,Y:] & ( for x, y being set st x in X & y in Y holds

b_{3} . (x,y) = x ) ) );

for X, Y being set

for b

( b

b

:: deftheorem Def5 defines pr2 FUNCT_3:def 5 :

for X, Y being set

for b_{3} being Function holds

( b_{3} = pr2 (X,Y) iff ( dom b_{3} = [:X,Y:] & ( for x, y being set st x in X & y in Y holds

b_{3} . (x,y) = y ) ) );

for X, Y being set

for b

( b

b

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

redefine func pr2 (X,Y) -> Function of [:X,Y:],Y;

coherence

pr2 (X,Y) is Function of [:X,Y:],Y

end;
:: original: pr1

redefine func pr1 (X,Y) -> Function of [:X,Y:],X;

coherence

pr1 (X,Y) is Function of [:X,Y:],X

proof end;

:: original: pr2redefine func pr2 (X,Y) -> Function of [:X,Y:],Y;

coherence

pr2 (X,Y) is Function of [:X,Y:],Y

proof end;

definition

let X be set ;

ex b_{1} being Function st

( dom b_{1} = X & ( for x being set st x in X holds

b_{1} . x = [x,x] ) )

for b_{1}, b_{2} being Function st dom b_{1} = X & ( for x being set st x in X holds

b_{1} . x = [x,x] ) & dom b_{2} = X & ( for x being set st x in X holds

b_{2} . x = [x,x] ) holds

b_{1} = b_{2}

end;
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 ( dom it = X & ( for x being set st x in X holds

it . x = [x,x] ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines delta FUNCT_3:def 6 :

for X being set

for b_{2} being Function holds

( b_{2} = delta X iff ( dom b_{2} = X & ( for x being set st x in X holds

b_{2} . x = [x,x] ) ) );

for X being set

for b

( b

b

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

end;
:: original: delta

redefine func delta X -> Function of X,[:X,X:];

coherence

delta X is Function of X,[:X,X:]

proof end;

:: Complex functions

definition

let f, g be Function;

ex b_{1} being Function st

( dom b_{1} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{1} holds

b_{1} . x = [(f . x),(g . x)] ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{1} holds

b_{1} . x = [(f . x),(g . x)] ) & dom b_{2} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{2} holds

b_{2} . x = [(f . x),(g . x)] ) holds

b_{1} = b_{2}

end;
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 ( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds

it . x = [(f . x),(g . x)] ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def7 defines <: FUNCT_3:def 7 :

for f, g, b_{3} being Function holds

( b_{3} = <:f,g:> iff ( dom b_{3} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{3} holds

b_{3} . x = [(f . x),(g . x)] ) ) );

for f, g, b

( b

b

registration

let f be empty Function;

let g be Function;

coherence

<:f,g:> is empty

<:g,f:> is empty

end;
let g be Function;

coherence

<:f,g:> is empty

proof end;

coherence <:g,f:> is empty

proof 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)]

for f, g being Function st x in (dom f) /\ (dom g) holds

<:f,g:> . x = [(f . x),(g . x)]

proof 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)]

for f, g being Function st dom f = X & dom g = X & x in X holds

<:f,g:> . x = [(f . x),(g . x)]

proof 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 )

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 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 )

( f = k & g = h )

proof 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)

for C being non empty set

for f, g being Function holds <:f,g:> " [:B,C:] = (f " B) /\ (g " C)

proof 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:]

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

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)]

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

for f being Function of X,Y

for g being Function of X,Z holds rng <:f,g:> c= [:Y,Z:]

proof 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 )

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

theorem :: FUNCT_3:62

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 )

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 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 )

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

:: Product-functions

definition

let f, g be Function;

ex b_{1} being Function st

( dom b_{1} = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds

b_{1} . (x,y) = [(f . x),(g . y)] ) )

for b_{1}, b_{2} being Function st dom b_{1} = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds

b_{1} . (x,y) = [(f . x),(g . y)] ) & dom b_{2} = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds

b_{2} . (x,y) = [(f . x),(g . y)] ) holds

b_{1} = b_{2}

end;
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 ( 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)] ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def8 defines [: FUNCT_3:def 8 :

for f, g, b_{3} being Function holds

( b_{3} = [:f,g:] iff ( dom b_{3} = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds

b_{3} . (x,y) = [(f . x),(g . y)] ) ) );

for f, g, b

( b

b

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)]

for x, y being set st [x,y] in [:(dom f),(dom g):] holds

[:f,g:] . (x,y) = [(f . x),(g . y)]

proof 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 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)

for f, g being Function st dom f = X & dom g = X holds

<:f,g:> = [:f,g:] * (delta X)

proof 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:]

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

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)]

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

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

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 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)

for f1 being Function of X,Y1

for f2 being Function of X,Y2 holds <:f1,f2:> = [:f1,f2:] * (delta X)

proof end;

begin

:: from AMI_1

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

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

registration

let A be set ;

ex b_{1} being BinOp of A st b_{1} is idempotent

end;
cluster Relation-like [:A,A:] -defined A -valued Function-like quasi_total idempotent for Element of bool [:[:A,A:],A:];

existence ex b

proof end;

registration

let A be set ;

let b be idempotent BinOp of A;

let a be Element of A;

reducibility

b . (a,a) = a by BINOP_1:def 4;

end;
let b be idempotent BinOp of A;

let a be Element of A;

reducibility

b . (a,a) = a by BINOP_1:def 4;