now for s1, s2 being SortSymbol of F1()
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 s1,
s2 be
SortSymbol of
F1();
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() . s2set R =
F4();
let f be
Function of
( the Sorts of F2() . s1),
( the Sorts of F2() . s2);
( 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]
;
for a, b being set st [a,b] in F4() . s1 holds
[(f . a),(f . b)] in F4() . s2let a,
b be
set ;
( [a,b] in F4() . s1 implies [(f . a),(f . b)] in F4() . s2 )assume A6:
[a,b] in F4()
. s1
;
[(f . a),(f . b)] in F4() . s2then A7:
b in the
Sorts of
F2()
. s1
by ZFMISC_1:87;
a in the
Sorts of
F2()
. s1
by A6, ZFMISC_1:87;
then consider s9 being
SortSymbol of
F1(),
f9 being
Function of
( the Sorts of F2() . s9),
( the Sorts of F2() . s1),
x,
y being
Element of
F2(),
s9 such that A8:
P1[
f9,
s9,
s1]
and A9:
[x,y] in F3()
. s9
and A10:
a = f9 . x
and A11:
b = f9 . y
by A4, A6, A7;
A12:
f . a = (f * f9) . x
by A10, FUNCT_2:15;
A13:
f . b = (f * f9) . y
by A11, FUNCT_2:15;
P1[
f * f9,
s9,
s2]
by A2, A5, A8;
hence
[(f . a),(f . b)] in F4()
. s2
by A4, A9, A12, A13;
verum end;
hence
P2[F4()]
by A1; ( F3() c= F4() & ( for P being ManySortedRelation of F2() st P2[P] & F3() c= P holds
F4() c= P ) )
thus
F3() c= F4()
for P being ManySortedRelation of F2() st P2[P] & F3() c= P holds
F4() c= Pproof
let i be
object ;
PBOOLE:def 2 ( not i in the carrier of F1() or F3() . i c= F4() . i )
assume
i in the
carrier of
F1()
;
F3() . i c= F4() . i
then reconsider s =
i as
SortSymbol of
F1() ;
F3()
. s c= F4()
. s
proof
set f =
id ( the Sorts of F2() . s);
let x,
y be
object ;
RELAT_1:def 3 ( not [x,y] in F3() . s or [x,y] in F4() . s )
assume A14:
[x,y] in F3()
. s
;
[x,y] in F4() . s
then reconsider a =
x,
b =
y as
Element of
F2(),
s by ZFMISC_1:87;
A15:
(id ( the Sorts of F2() . s)) . b = b
;
A16:
P1[
id ( the Sorts of F2() . s),
s,
s]
by A3;
(id ( the Sorts of F2() . s)) . a = a
;
hence
[x,y] in F4()
. s
by A4, A14, A16, A15;
verum
end;
hence
F3()
. i c= F4()
. i
;
verum
end;
let P be ManySortedRelation of F2(); ( P2[P] & F3() c= P implies F4() c= P )
assume that
A17:
P2[P]
and
A18:
F3() c= P
; F4() c= P
let i be object ; PBOOLE:def 2 ( not i in the carrier of F1() or F4() . i c= P . i )
assume
i in the carrier of F1()
; F4() . i c= P . i
then reconsider s = i as SortSymbol of F1() ;
F4() . s c= P . s
proof
let x,
y be
object ;
RELAT_1:def 3 ( not [x,y] in F4() . s or [x,y] in P . s )
assume A19:
[x,y] in F4()
. s
;
[x,y] in P . s
then reconsider a =
x,
b =
y as
Element of
F2(),
s by ZFMISC_1:87;
consider s9 being
SortSymbol of
F1(),
f being
Function of
( the Sorts of F2() . s9),
( the Sorts of F2() . s),
u,
v being
Element of
F2(),
s9 such that A20:
P1[
f,
s9,
s]
and A21:
[u,v] in F3()
. s9
and A22:
a = f . u
and A23:
b = f . v
by A4, A19;
F3()
. s9 c= P . s9
by A18;
hence
[x,y] in P . s
by A1, A17, A20, A21, A22, A23;
verum
end;
hence
F4() . i c= P . i
; verum