:: by J\'ozef Bia{\l}as

::

:: Received October 27, 1989

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

definition

let X be set ;

let F be BinOp of X;

ex b_{1} being Subset of X st

for x being set st x in [:b_{1},b_{1}:] holds

F . x in b_{1}

end;
let F be BinOp of X;

mode Preserv of F -> Subset of X means :Def1: :: REALSET1:def 1

for x being set st x in [:it,it:] holds

F . x in it;

existence for x being set st x in [:it,it:] holds

F . x in it;

ex b

for x being set st x in [:b

F . x in b

proof end;

:: deftheorem Def1 defines Preserv REALSET1:def 1 :

for X being set

for F being BinOp of X

for b_{3} being Subset of X holds

( b_{3} is Preserv of F iff for x being set st x in [:b_{3},b_{3}:] holds

F . x in b_{3} );

for X being set

for F being BinOp of X

for b

( b

F . x in b

:: deftheorem defines || REALSET1:def 2 :

for R being Relation

for A being set holds R || A = R | [:A,A:];

for R being Relation

for A being set holds R || A = R | [:A,A:];

definition

let X be set ;

let F be BinOp of X;

let A be Preserv of F;

:: original: ||

redefine func F || A -> BinOp of A;

coherence

F || A is BinOp of A by Th2;

end;
let F be BinOp of X;

let A be Preserv of F;

:: original: ||

redefine func F || A -> BinOp of A;

coherence

F || A is BinOp of A by Th2;

definition

let X be non trivial set ;

let F be BinOp of X;

let x be Element of X;

;

end;
let F be BinOp of X;

let x be Element of X;

pred F is_Bin_Op_Preserv x means :: REALSET1:def 3

( X \ {x} is Preserv of F & (F || X) \ {x} is BinOp of (X \ {x}) );

correctness ( X \ {x} is Preserv of F & (F || X) \ {x} is BinOp of (X \ {x}) );

;

:: deftheorem defines is_Bin_Op_Preserv REALSET1:def 3 :

for X being non trivial set

for F being BinOp of X

for x being Element of X holds

( F is_Bin_Op_Preserv x iff ( X \ {x} is Preserv of F & (F || X) \ {x} is BinOp of (X \ {x}) ) );

for X being non trivial set

for F being BinOp of X

for x being Element of X holds

( F is_Bin_Op_Preserv x iff ( X \ {x} is Preserv of F & (F || X) \ {x} is BinOp of (X \ {x}) ) );

::$CT 2

theorem Th3: :: REALSET1:5

for X being set

for A being Subset of X ex F being BinOp of X st

for x being set st x in [:A,A:] holds

F . x in A

for A being Subset of X ex F being BinOp of X st

for x being set st x in [:A,A:] holds

F . x in A

proof end;

definition

let X be set ;

let A be Subset of X;

ex b_{1} being BinOp of X st

for x being set st x in [:A,A:] holds

b_{1} . x in A
by Th3;

end;
let A be Subset of X;

mode Presv of X,A -> BinOp of X means :Def4: :: REALSET1:def 4

for x being set st x in [:A,A:] holds

it . x in A;

existence for x being set st x in [:A,A:] holds

it . x in A;

ex b

for x being set st x in [:A,A:] holds

b

:: deftheorem Def4 defines Presv REALSET1:def 4 :

for X being set

for A being Subset of X

for b_{3} being BinOp of X holds

( b_{3} is Presv of X,A iff for x being set st x in [:A,A:] holds

b_{3} . x in A );

for X being set

for A being Subset of X

for b

( b

b

definition
end;

:: deftheorem defines ||| REALSET1:def 5 :

for X being set

for A being Subset of X

for F being Presv of X,A holds F ||| A = F || A;

for X being set

for A being Subset of X

for F being Presv of X,A holds F ||| A = F || A;

definition

let A be set ;

let x be Element of A;

ex b_{1} being BinOp of A st

for y being set st y in [:(A \ {x}),(A \ {x}):] holds

b_{1} . y in A \ {x}
by Th3;

end;
let x be Element of A;

mode DnT of x,A -> BinOp of A means :Def6: :: REALSET1:def 6

for y being set st y in [:(A \ {x}),(A \ {x}):] holds

it . y in A \ {x};

existence for y being set st y in [:(A \ {x}),(A \ {x}):] holds

it . y in A \ {x};

ex b

for y being set st y in [:(A \ {x}),(A \ {x}):] holds

b

:: deftheorem Def6 defines DnT REALSET1:def 6 :

for A being set

for x being Element of A

for b_{3} being BinOp of A holds

( b_{3} is DnT of x,A iff for y being set st y in [:(A \ {x}),(A \ {x}):] holds

b_{3} . y in A \ {x} );

for A being set

for x being Element of A

for b

( b

b

theorem Th5: :: REALSET1:7

for A being non trivial set

for x being Element of A

for F being DnT of x,A holds F || (A \ {x}) is BinOp of (A \ {x})

for x being Element of A

for F being DnT of x,A holds F || (A \ {x}) is BinOp of (A \ {x})

proof end;

definition

let A be non trivial set ;

let x be Element of A;

let F be DnT of x,A;

coherence

F || (A \ {x}) is BinOp of (A \ {x}) by Th5;

end;
let x be Element of A;

let F be DnT of x,A;

coherence

F || (A \ {x}) is BinOp of (A \ {x}) by Th5;

:: deftheorem defines ! REALSET1:def 7 :

for A being non trivial set

for x being Element of A

for F being DnT of x,A holds F ! (A,x) = F || (A \ {x});

for A being non trivial set

for x being Element of A

for F being DnT of x,A holds F ! (A,x) = F || (A \ {x});