:: Group and Field Definitions
:: by J\'ozef Bia{\l}as
::
:: Received October 27, 1989
:: Copyright (c) 1990-2018 Association of Mizar Users

theorem Th1: :: REALSET1:1
for X, x being set
for F being Function of [:X,X:],X st x in [:X,X:] holds
F . x in X
proof end;

definition
let X be set ;
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
ex b1 being Subset of X st
for x being set st x in [:b1,b1:] holds
F . x in b1
proof end;
end;

:: deftheorem Def1 defines Preserv REALSET1:def 1 :
for X being set
for F being BinOp of X
for b3 being Subset of X holds
( b3 is Preserv of F iff for x being set st x in [:b3,b3:] holds
F . x in b3 );

definition
let R be Relation;
let A be set ;
func R || A -> set equals :: REALSET1:def 2
R | [:A,A:];
coherence
R | [:A,A:] is set
;
end;

:: deftheorem defines || REALSET1:def 2 :
for R being Relation
for A being set holds R || A = R | [:A,A:];

registration
let R be Relation;
let A be set ;
coherence
R || A is Relation-like
;
end;

registration
let R be Function;
let A be set ;
coherence
R || A is Function-like
;
end;

theorem Th2: :: REALSET1:2
for X being set
for F being BinOp of X
for A being Preserv of F holds F || A is BinOp of A
proof end;

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;

definition
let X be non trivial set ;
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
;
end;

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

theorem :: REALSET1:3
canceled;

theorem :: REALSET1:4
canceled;

::\$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
proof end;

definition
let X be set ;
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
ex b1 being BinOp of X st
for x being set st x in [:A,A:] holds
b1 . x in A
by Th3;
end;

:: deftheorem Def4 defines Presv REALSET1:def 4 :
for X being set
for A being Subset of X
for b3 being BinOp of X holds
( b3 is Presv of X,A iff for x being set st x in [:A,A:] holds
b3 . x in A );

theorem Th4: :: REALSET1:6
for X being set
for A being Subset of X
for F being Presv of X,A holds F || A is BinOp of A
proof end;

definition
let X be set ;
let A be Subset of X;
let F be Presv of X,A;
func F ||| A -> BinOp of A equals :: REALSET1:def 5
F || A;
coherence
F || A is BinOp of A
by Th4;
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;

definition
let A be set ;
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
ex b1 being BinOp of A st
for y being set st y in [:(A \ {x}),(A \ {x}):] holds
b1 . y in A \ {x}
by Th3;
end;

:: deftheorem Def6 defines DnT REALSET1:def 6 :
for A being set
for x being Element of A
for b3 being BinOp of A holds
( b3 is DnT of x,A iff for y being set st y in [:(A \ {x}),(A \ {x}):] holds
b3 . y in A \ {x} );

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})
proof end;

definition
let A be non trivial set ;
let x be Element of A;
let F be DnT of x,A;
func F ! (A,x) -> BinOp of (A \ {x}) equals :: REALSET1:def 7
F || (A \ {x});
coherence
F || (A \ {x}) is BinOp of (A \ {x})
by Th5;
end;

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