let A be non trivial set ; :: thesis: for B, Bo1 being set
for yo1 being Function of Bo1,A
for Bo2 being set
for yo2 being Function of Bo2,A st Bo1 c= B & Bo2 c= B & cylinder0 A,B,Bo1,yo1 = cylinder0 A,B,Bo2,yo2 holds
( Bo1 = Bo2 & yo1 = yo2 )
let B, Bo1 be set ; :: thesis: for yo1 being Function of Bo1,A
for Bo2 being set
for yo2 being Function of Bo2,A st Bo1 c= B & Bo2 c= B & cylinder0 A,B,Bo1,yo1 = cylinder0 A,B,Bo2,yo2 holds
( Bo1 = Bo2 & yo1 = yo2 )
let yo1 be Function of Bo1,A; :: thesis: for Bo2 being set
for yo2 being Function of Bo2,A st Bo1 c= B & Bo2 c= B & cylinder0 A,B,Bo1,yo1 = cylinder0 A,B,Bo2,yo2 holds
( Bo1 = Bo2 & yo1 = yo2 )
let Bo2 be set ; :: thesis: for yo2 being Function of Bo2,A st Bo1 c= B & Bo2 c= B & cylinder0 A,B,Bo1,yo1 = cylinder0 A,B,Bo2,yo2 holds
( Bo1 = Bo2 & yo1 = yo2 )
let yo2 be Function of Bo2,A; :: thesis: ( Bo1 c= B & Bo2 c= B & cylinder0 A,B,Bo1,yo1 = cylinder0 A,B,Bo2,yo2 implies ( Bo1 = Bo2 & yo1 = yo2 ) )
assume AS: ( Bo1 c= B & Bo2 c= B & cylinder0 A,B,Bo1,yo1 = cylinder0 A,B,Bo2,yo2 ) ; :: thesis: ( Bo1 = Bo2 & yo1 = yo2 )
P1: { y where y is Function of B,A : y | Bo1 = yo1 } = cylinder0 A,B,Bo1,yo1 by DefX01, AS;
P2: { y where y is Function of B,A : y | Bo2 = yo2 } = cylinder0 A,B,Bo2,yo2 by DefX01, AS;
hence Bo1 = Bo2 by Lm2, AS, P1; :: thesis: yo1 = yo2
consider y0 being set such that
P4: y0 in { y where y is Function of B,A : y | Bo1 = yo1 } by P1, XBOOLE_0:def 1;
consider y being Function of B,A such that
P5: ( y0 = y & y | Bo1 = yo1 ) by P4;
consider w being Function of B,A such that
P6: ( y0 = w & w | Bo2 = yo2 ) by P1, P2, AS, P4;
thus yo1 = yo2 by Lm2, AS, P1, P2, P5, P6; :: thesis: verum