set Bo = {} ;
set yo = the Function of {},A;
take cylinder0 (A,B,{}, the Function of {},A) ; :: thesis: ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & cylinder0 (A,B,{}, the Function of {},A) = cylinder0 (A,B,Bo,yo) )
{} is Subset of B by XBOOLE_1:2;
hence ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & cylinder0 (A,B,{}, the Function of {},A) = cylinder0 (A,B,Bo,yo) ) ; :: thesis: verum