src/ZF/Constructible/Relative.thy
changeset 13323 2c287f50c9f3
parent 13319 23de7b3af453
child 13339 0f89104dd377
     1.1 --- a/src/ZF/Constructible/Relative.thy	Tue Jul 09 13:41:38 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Tue Jul 09 15:39:44 2002 +0200
     1.3 @@ -104,8 +104,9 @@
     1.4    composition :: "[i=>o,i,i,i] => o"
     1.5      "composition(M,r,s,t) == 
     1.6          \<forall>p[M]. p \<in> t <-> 
     1.7 -               (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. pair(M,x,z,p) & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r)"
     1.8 -
     1.9 +               (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
    1.10 +                pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
    1.11 +                xy \<in> s & yz \<in> r)"
    1.12  
    1.13    injection :: "[i=>o,i,i,i] => o"
    1.14      "injection(M,A,B,f) ==