begin
scheme
FraenkelA2{
F1()
-> non
empty set ,
F2(
set ,
set )
-> set ,
P1[
set ,
set ],
P2[
set ,
set ] } :
{ F2(s,t) where s, t is Element of F1() : P1[s,t] } is
Subset of
F1()
provided
A1:
for
s,
t being
Element of
F1() holds
F2(
s,
t)
in F1()
Lm1:
for x, a1, a2, b1, b2 being set st x = [[a1,a2],[b1,b2]] holds
( (x `1) `1 = a1 & (x `1) `2 = a2 & (x `2) `1 = b1 & (x `2) `2 = b2 )
begin
definition
let P,
R be
Relation;
func ["P,R"] -> Relation means :
Def1:
for
x,
y being
set holds
(
[x,y] in it iff ex
p,
q,
s,
t being
set st
(
x = [p,q] &
y = [s,t] &
[p,s] in P &
[q,t] in R ) );
existence
ex b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) )
uniqueness
for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) holds
b1 = b2
end;
::
deftheorem Def1 defines
[" YELLOW_3:def 1 :
for P, R, b3 being Relation holds
( b3 = ["P,R"] iff for x, y being set holds
( [x,y] in b3 iff ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) );
theorem Th10:
for
P,
R being
Relation for
x being
set holds
(
x in ["P,R"] iff (
[((x `1) `1),((x `2) `1)] in P &
[((x `1) `2),((x `2) `2)] in R & ex
a,
b being
set st
x = [a,b] & ex
c,
d being
set st
x `1 = [c,d] & ex
e,
f being
set st
x `2 = [e,f] ) )
definition
let A,
B,
X,
Y be
set ;
let P be
Relation of
A,
B;
let R be
Relation of
X,
Y;
["redefine func ["P,R"] -> Relation of
[:A,X:],
[:B,Y:];
coherence
["P,R"] is Relation of [:A,X:],[:B,Y:]
end;