now :: thesis: 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() . s2
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() . s2
set 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() . s2
let 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() . s2
then 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; :: 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= P
proof
let i be object ; :: according to PBOOLE:def 2 :: 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 object ; :: 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: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; :: 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 object ; :: according to PBOOLE:def 2 :: 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 object ; :: 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: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; :: thesis: verum
end;
hence F4() . i c= P . i ; :: thesis: verum