let C1, C2 be Coherence_Space; :: thesis: for X being Subset of [:C1,(union C2):] st ( for x being set st x in X holds
x `1 is finite ) & ( for a, b being finite Element of C1 st a c= b holds
for y being set st [a,y] in X holds
[b,y] in X ) & ( for a being finite Element of C1
for y1, y2 being set st [a,y1] in X & [a,y2] in X holds
{y1,y2} in C2 ) holds
ex f being U-continuous Function of C1,C2 st X = graph f
let X be Subset of [:C1,(union C2):]; :: thesis: ( ( for x being set st x in X holds
x `1 is finite ) & ( for a, b being finite Element of C1 st a c= b holds
for y being set st [a,y] in X holds
[b,y] in X ) & ( for a being finite Element of C1
for y1, y2 being set st [a,y1] in X & [a,y2] in X holds
{y1,y2} in C2 ) implies ex f being U-continuous Function of C1,C2 st X = graph f )
assume A1: ( ( for x being set st x in X holds
x `1 is finite ) & ( for a, b being finite Element of C1 st a c= b holds
for y being set st [a,y] in X holds
[b,y] in X ) & ( for a being finite Element of C1
for y1, y2 being set st [a,y1] in X & [a,y2] in X holds
{y1,y2} in C2 ) & ( for f being U-continuous Function of C1,C2 holds not X = graph f ) ) ; :: thesis: contradiction
then ex f being U-continuous Function of C1,C2 st
( X = graph f & ( for a being Element of C1 holds f . a = X .: (Fin a) ) ) by Lm4;
hence contradiction by A1; :: thesis: verum