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 that
A1: Bo1 c= B and
A2: Bo2 c= B and
A3: cylinder0 (A,B,Bo1,yo1) = cylinder0 (A,B,Bo2,yo2) ; :: thesis: ( Bo1 = Bo2 & yo1 = yo2 )
A4: { y where y is Function of B,A : y | Bo1 = yo1 } = cylinder0 (A,B,Bo1,yo1) by A1, Def1;
then consider y0 being object such that
A5: y0 in { y where y is Function of B,A : y | Bo1 = yo1 } by XBOOLE_0:def 1;
A6: ex y being Function of B,A st
( y0 = y & y | Bo1 = yo1 ) by A5;
A7: { y where y is Function of B,A : y | Bo2 = yo2 } = cylinder0 (A,B,Bo2,yo2) by A2, Def1;
hence Bo1 = Bo2 by A1, A2, A3, A4, Lm4; :: thesis: yo1 = yo2
ex w being Function of B,A st
( y0 = w & w | Bo2 = yo2 ) by A3, A4, A7, A5;
hence yo1 = yo2 by A1, A2, A3, A4, A7, A6, Lm4; :: thesis: verum