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 Th1;
hence ex b₁ being finite Subset of 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 } & b₁ = Bo ) ; :: thesis: verum