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

::

:: Received October 27, 1989

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

definition

let X be set ;

let F be BinOp of X;

let A be Subset of X;

end;
let F be BinOp of X;

let A be Subset of X;

attr A is F -binopclosed means :Def1: :: REALSET1:def 1

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

F . x in A;

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

F . x in A;

:: deftheorem Def1 defines -binopclosed REALSET1:def 1 :

for X being set

for F being BinOp of X

for A being Subset of X holds

( A is F -binopclosed iff for x being set st x in [:A,A:] holds

F . x in A );

for X being set

for F being BinOp of X

for A being Subset of X holds

( A is F -binopclosed iff for x being set st x in [:A,A:] holds

F . x in A );

registration

let X be set ;

let F be BinOp of X;

existence

ex b_{1} being Subset of X st b_{1} is F -binopclosed

end;
let F be BinOp of X;

existence

ex b

proof end;

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

theorem Th2: :: REALSET1:2

for X being set

for F being BinOp of X

for A being b_{2} -binopclosed Subset of X holds F || A is BinOp of A

for F being BinOp of X

for A being b

proof end;

definition

let X be set ;

let F be BinOp of X;

let A be F -binopclosed Subset of X;

:: 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 F -binopclosed Subset of X;

:: original: ||

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

coherence

F || A is BinOp of A by Th2;

::$CT 2

definition

let X be set ;

let A be Subset of X;

let F be BinOp of X;

end;
let A be Subset of X;

let F be BinOp of X;

attr F is A -subsetpreserving means :Def4: :: REALSET1:def 4

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

F . x in A;

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

F . x in A;

:: deftheorem Def4 defines -subsetpreserving REALSET1:def 4 :

for X being set

for A being Subset of X

for F being BinOp of X holds

( F is A -subsetpreserving iff for x being set st x in [:A,A:] holds

F . x in A );

for X being set

for A being Subset of X

for F being BinOp of X holds

( F is A -subsetpreserving iff for x being set st x in [:A,A:] holds

F . x in A );

registration

let X be set ;

let A be Subset of X;

ex b_{1} being BinOp of X st b_{1} is A -subsetpreserving

end;
let A be Subset of X;

cluster Relation-like [:X,X:] -defined X -valued Function-like V14([:X,X:]) V18([:X,X:],X) A -subsetpreserving for Element of bool [:[:X,X:],X:];

existence ex b

proof end;

definition
end;

theorem Th4: :: REALSET1:6

for X being set

for A being Subset of X

for F being b_{2} -subsetpreserving BinOp of X holds F || A is BinOp of A

for A being Subset of X

for F being b

proof end;

definition

let X be set ;

let A be Subset of X;

let F be A -subsetpreserving BinOp of X;

coherence

F || A is BinOp of A by Th4;

end;
let A be Subset of X;

let F be A -subsetpreserving BinOp of X;

coherence

F || A is BinOp of A by Th4;

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

for X being set

for A being Subset of X

for F being b_{2} -subsetpreserving BinOp of X holds F ||| A = F || A;

for X being set

for A being Subset of X

for F being b

theorem Th5: :: REALSET1:7

for A being non trivial set

for x being Element of A

for F being b_{1} \ {b_{2}} -subsetpreserving BinOp of A holds F || (A \ {x}) is BinOp of (A \ {x})

for x being Element of A

for F being b

proof end;

definition

let A be non trivial set ;

let x be Element of A;

let F be A \ {x} -subsetpreserving BinOp of A;

coherence

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

end;
let x be Element of A;

let F be A \ {x} -subsetpreserving BinOp of 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 b_{1} \ {b_{2}} -subsetpreserving BinOp of A holds F ! (A,x) = F || (A \ {x});

for A being non trivial set

for x being Element of A

for F being b