let A be non empty set ; :: thesis: for B being set
for D being thin_cylinder of A,B ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D = { y where y is Function of B,A : y | Bo = yo } )
let B be set ; :: thesis: for D being thin_cylinder of A,B ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D = { y where y is Function of B,A : y | Bo = yo } )
let D be thin_cylinder of A,B; :: thesis: ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D = { y where y is Function of B,A : y | Bo = yo } )
consider Bo being Subset of B, yo being Function of Bo,A such that
A1: ( Bo is finite & D = cylinder0 A,B,Bo,yo ) by Def21;
D = { y where y is Function of B,A : y | Bo = yo } by DefX01, A1;
hence ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D = { y where y is Function of B,A : y | Bo = yo } ) by A1; :: thesis: verum