now set R =
F4();
let s1,
s2 be
SortSymbol of
F1();
:: thesis: for f being Function of (the Sorts of F2() . s1),(the Sorts of F2() . s2) st P1[f,s1,s2] holds
for a, b being set st [a,b] in F4() . s1 holds
[(f . a),(f . b)] in F4() . s2let f be
Function of
(the Sorts of F2() . s1),
(the Sorts of F2() . s2);
:: thesis: ( P1[f,s1,s2] implies for a, b being set st [a,b] in F4() . s1 holds
[(f . a),(f . b)] in F4() . s2 )assume A5:
P1[
f,
s1,
s2]
;
:: thesis: for a, b being set st [a,b] in F4() . s1 holds
[(f . a),(f . b)] in F4() . s2let a,
b be
set ;
:: thesis: ( [a,b] in F4() . s1 implies [(f . a),(f . b)] in F4() . s2 )assume A6:
[a,b] in F4()
. s1
;
:: thesis: [(f . a),(f . b)] in F4() . s2then
(
a in the
Sorts of
F2()
. s1 &
b in the
Sorts of
F2()
. s1 )
by ZFMISC_1:106;
then consider s' being
SortSymbol of
F1(),
f' being
Function of
(the Sorts of F2() . s'),
(the Sorts of F2() . s1),
x,
y being
Element of
F2(),
s' such that A7:
(
P1[
f',
s',
s1] &
[x,y] in F3()
. s' &
a = f' . x &
b = f' . y )
by A4, A6;
A8:
P1[
f * f',
s',
s2]
by A2, A5, A7;
(
f . a = (f * f') . x &
f . b = (f * f') . y )
by A7, FUNCT_2:21;
hence
[(f . a),(f . b)] in F4()
. s2
by A4, A7, A8;
:: thesis: verum end;
hence
P2[F4()]
by A1; :: thesis: ( F3() c= F4() & ( for P being ManySortedRelation of F2() st P2[P] & F3() c= P holds
F4() c= P ) )
thus
F3() c= F4()
:: thesis: for P being ManySortedRelation of F2() st P2[P] & F3() c= P holds
F4() c= Pproof
let i be
set ;
:: according to PBOOLE:def 5 :: thesis: ( not i in the carrier of F1() or F3() . i c= F4() . i )
assume
i in the
carrier of
F1()
;
:: thesis: F3() . i c= F4() . i
then reconsider s =
i as
SortSymbol of
F1() ;
F3()
. s c= F4()
. s
proof
let x,
y be
set ;
:: according to RELAT_1:def 3 :: thesis: ( not [x,y] in F3() . s or [x,y] in F4() . s )
assume A9:
[x,y] in F3()
. s
;
:: thesis: [x,y] in F4() . s
then reconsider a =
x,
b =
y as
Element of
F2(),
s by ZFMISC_1:106;
set f =
id (the Sorts of F2() . s);
(
P1[
id (the Sorts of F2() . s),
s,
s] &
(id (the Sorts of F2() . s)) . a = a &
(id (the Sorts of F2() . s)) . b = b )
by A3, FUNCT_1:34;
hence
[x,y] in F4()
. s
by A4, A9;
:: thesis: verum
end;
hence
F3()
. i c= F4()
. i
;
:: thesis: verum
end;
let P be ManySortedRelation of F2(); :: thesis: ( P2[P] & F3() c= P implies F4() c= P )
assume A10:
( P2[P] & F3() c= P )
; :: thesis: F4() c= P
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in the carrier of F1() or F4() . i c= P . i )
assume
i in the carrier of F1()
; :: thesis: F4() . i c= P . i
then reconsider s = i as SortSymbol of F1() ;
F4() . s c= P . s
proof
let x,
y be
set ;
:: according to RELAT_1:def 3 :: thesis: ( not [x,y] in F4() . s or [x,y] in P . s )
assume A11:
[x,y] in F4()
. s
;
:: thesis: [x,y] in P . s
then reconsider a =
x,
b =
y as
Element of
F2(),
s by ZFMISC_1:106;
consider s' being
SortSymbol of
F1(),
f being
Function of
(the Sorts of F2() . s'),
(the Sorts of F2() . s),
u,
v being
Element of
F2(),
s' such that A12:
(
P1[
f,
s',
s] &
[u,v] in F3()
. s' &
a = f . u &
b = f . v )
by A4, A11;
F3()
. s' c= P . s'
by A10, PBOOLE:def 5;
hence
[x,y] in P . s
by A1, A10, A12;
:: thesis: verum
end;
hence
F4() . i c= P . i
; :: thesis: verum