now 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() . s2set R =
F4();
let 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 A7:
b in the
Sorts of
F2()
. s1
by ZFMISC_1:106;
a in the
Sorts of
F2()
. s1
by A6, 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 A8:
P1[
f',
s',
s1]
and A9:
[x,y] in F3()
. s'
and A10:
a = f' . x
and A11:
b = f' . y
by A4, A6, A7;
A12:
f . a = (f * f') . x
by A10, FUNCT_2:21;
A13:
f . b = (f * f') . y
by A11, FUNCT_2:21;
P1[
f * f',
s',
s2]
by A2, A5, A8;
hence
[(f . a),(f . b)] in F4()
. s2
by A4, A9, A12, A13;
:: 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
set f =
id (the Sorts of F2() . s);
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 A14:
[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;
A15:
(id (the Sorts of F2() . s)) . b = b
by FUNCT_1:34;
A16:
P1[
id (the Sorts of F2() . s),
s,
s]
by A3;
(id (the Sorts of F2() . s)) . a = a
by FUNCT_1:34;
hence
[x,y] in F4()
. s
by A4, A14, A16, A15;
:: 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 that
A17:
P2[P]
and
A18:
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 A19:
[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 A20:
P1[
f,
s',
s]
and A21:
[u,v] in F3()
. s'
and A22:
a = f . u
and A23:
b = f . v
by A4, A19;
F3()
. s' c= P . s'
by A18, PBOOLE:def 5;
hence
[x,y] in P . s
by A1, A17, A20, A21, A22, A23;
:: thesis: verum
end;
hence
F4() . i c= P . i
; :: thesis: verum