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 and
A2: D = cylinder0 (A,B,Bo,yo) by Def2;
D = { y where y is Function of B,A : y | Bo = yo } by A2, Def1;
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