let A be non trivial set ; :: thesis: for B being set
for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st Bo1 <> Bo2 holds
{ y where y is Function of B,A : y | Bo1 = yo1 } <> { y where y is Function of B,A : y | Bo2 = yo2 }
let B be set ; :: thesis: for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st Bo1 <> Bo2 holds
{ y where y is Function of B,A : y | Bo1 = yo1 } <> { y where y is Function of B,A : y | Bo2 = yo2 }
let Bo1, Bo2 be Subset of B; :: thesis: for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st Bo1 <> Bo2 holds
{ y where y is Function of B,A : y | Bo1 = yo1 } <> { y where y is Function of B,A : y | Bo2 = yo2 }
let yo1 be Function of Bo1,A; :: thesis: for yo2 being Function of Bo2,A st Bo1 <> Bo2 holds
{ y where y is Function of B,A : y | Bo1 = yo1 } <> { y where y is Function of B,A : y | Bo2 = yo2 }
let yo2 be Function of Bo2,A; :: thesis: ( Bo1 <> Bo2 implies { y where y is Function of B,A : y | Bo1 = yo1 } <> { y where y is Function of B,A : y | Bo2 = yo2 } )
assume A1: Bo1 <> Bo2 ; :: thesis: { y where y is Function of B,A : y | Bo1 = yo1 } <> { y where y is Function of B,A : y | Bo2 = yo2 }
per cases ( not Bo2 c= Bo1 or Bo2 c= Bo1 ) ;
suppose not Bo2 c= Bo1 ; :: thesis: { y where y is Function of B,A : y | Bo1 = yo1 } <> { y where y is Function of B,A : y | Bo2 = yo2 }
then consider f being Function of B,A such that
A2: f | Bo1 = yo1 and
A3: f | Bo2 <> yo2 by Lm2;
not f in { y where y is Function of B,A : y | Bo2 = yo2 }
proof
assume f in { y where y is Function of B,A : y | Bo2 = yo2 } ; :: thesis: contradiction
then ex y being Function of B,A st
( f = y & y | Bo2 = yo2 ) ;
hence contradiction by A3; :: thesis: verum
end;
hence { y where y is Function of B,A : y | Bo1 = yo1 } <> { y where y is Function of B,A : y | Bo2 = yo2 } by A2; :: thesis: verum
end;
suppose Bo2 c= Bo1 ; :: thesis: { y where y is Function of B,A : y | Bo1 = yo1 } <> { y where y is Function of B,A : y | Bo2 = yo2 }
then consider f being Function of B,A such that
A4: f | Bo2 = yo2 and
A5: f | Bo1 <> yo1 by A1, Lm3;
not f in { y where y is Function of B,A : y | Bo1 = yo1 }
proof
assume f in { y where y is Function of B,A : y | Bo1 = yo1 } ; :: thesis: contradiction
then ex y being Function of B,A st
( f = y & y | Bo1 = yo1 ) ;
hence contradiction by A5; :: thesis: verum
end;
hence { y where y is Function of B,A : y | Bo1 = yo1 } <> { y where y is Function of B,A : y | Bo2 = yo2 } by A4; :: thesis: verum
end;
end;